src/HOL/Imperative_HOL/Heap_Monad.thy

     let
       val dummy_name = "";
       val dummy_type = ITyVar dummy_name;
       val dummy_case_term = IVar dummy_name;
       (*assumption: dummy values are not relevant for serialization*)
-      val unitt = IConst (unit', ([], []));
+      val unitt = IConst (unit', (([], []), []));
       fun dest_abs ((v, ty) `|-> t, _) = ((v, ty), t)
         | dest_abs (t, ty) =
             let
               val vs = Code_Thingol.fold_varnames cons t [];
               val v = Name.variant vs "x";

         | (t, ts) => imp_monad_bind bind' return' unit' t `$$ map (imp_monad_bind bind' return' unit') ts)
     | imp_monad_bind bind' return' unit' (v_ty `|-> t) = v_ty `|-> imp_monad_bind bind' return' unit' t
     | imp_monad_bind bind' return' unit' (ICase (((t, ty), pats), t0)) = ICase
         (((imp_monad_bind bind' return' unit' t, ty), (map o pairself) (imp_monad_bind bind' return' unit') pats), imp_monad_bind bind' return' unit' t0);
 
-   fun imp_program naming = (Graph.map_nodes o map_terms_stmt)
-     (imp_monad_bind (lookup naming @{const_name bindM})
-       (lookup naming @{const_name return})
-       (lookup naming @{const_name Unity}));
+  fun imp_program naming = (Graph.map_nodes o map_terms_stmt)
+    (imp_monad_bind (lookup naming @{const_name bindM})
+      (lookup naming @{const_name return})
+      (lookup naming @{const_name Unity}));
 
 in
 
   Code_Target.extend_target ("SML_imp", ("SML", imp_program))
   #> Code_Target.extend_target ("OCaml_imp", ("OCaml", imp_program))