fix bug introduced by removing open for records

by reverting

src/Ledger/Chain.lagda

@@ -37,8 +37,6 @@ private variable
   s : ChainState
   b : Block
   ls' : LState
-  es : EnactState
-  eps : EpochState
   nes : NewEpochState
 
 instance _ = +-0-monoid
@@ -102,16 +100,17 @@ data
 \end{code}
 \begin{figure*}[h]
 \begin{code}
-  CHAIN : record { stakeDistrs = calculateStakeDistrs (EpochState.ls eps) }
-          ⊢ ChainState.newEpochState s ⇀⦇ epoch (Block.slot b) ,NEWEPOCH⦈ nes
-          →  ⟦ Block.slot b , (EnactState.constitution es) .proj₁ .proj₂
-             , (EnactState.pparams es) .proj₁ , (EpochState.es eps) ⟧ˡᵉ
-          ⊢ EpochState.ls eps ⇀⦇ Block.ts b ,LEDGERS⦈ ls'
+ CHAIN :
+    let open ChainState s; open Block b; open NewEpochState newEpochState
+        open EpochState epochState; open EnactState es
+    in
+       record { stakeDistrs = calculateStakeDistrs ls }
+         ⊢ newEpochState ⇀⦇ epoch slot ,NEWEPOCH⦈ nes
+    →  ⟦ slot , constitution .proj₁ .proj₂ , pparams .proj₁ , es ⟧ˡᵉ
+         ⊢ ls ⇀⦇ ts ,LEDGERS⦈ ls'
     ────────────────────────────────
     _ ⊢ s ⇀⦇ b ,CHAIN⦈
-        record s { newEpochState =
-                   record nes { epochState =
-                                record (NewEpochState.epochState nes) { ls = ls'} } }
+        record s { newEpochState = record nes { epochState = record epochState { ls = ls'} } }
 \end{code}
 \end{AgdaMulticode}
 \caption{CHAIN transition system}