diff --git a/src/Ledger/Chain.lagda b/src/Ledger/Chain.lagda
index 82cedb217..377a9b52d 100644
--- a/src/Ledger/Chain.lagda
+++ b/src/Ledger/Chain.lagda
@@ -84,12 +84,10 @@ calculateStakeDistrs ls =
     { stakeDistr = govActionDeposits ls
     }
 
+data
 \end{code}
 \begin{figure*}[h]
 \begin{AgdaMulticode}
-\begin{code}[hide]
-data
-\end{code}
 \begin{code}
   _⊢_⇀⦇_,CHAIN⦈_ : ⊤ → ChainState → Block → ChainState → Set
 \end{code}
@@ -100,7 +98,7 @@ data
 \end{code}
 \begin{figure*}[h]
 \begin{code}
- CHAIN :
+  CHAIN :
     let open ChainState s; open Block b; open NewEpochState newEpochState
         open EpochState epochState; open EnactState es
     in