src/HOL/Imperative_HOL/Heap_Monad.thy

       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', (([], []), []));
-      fun dest_abs ((v, ty) `|-> t, _) = ((v, ty), t)
+      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";
               val ty' = (hd o fst o Code_Thingol.unfold_fun) ty;

       and tr_bind'' t = case Code_Thingol.unfold_app t
            of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if c = bind'
                 then tr_bind' [(x1, ty1), (x2, ty2)]
                 else force t
             | _ => force t;
-    in (dummy_name, dummy_type) `|-> ICase (((IVar dummy_name, dummy_type),
+    in (dummy_name, dummy_type) `|=> ICase (((IVar dummy_name, dummy_type),
       [(unitt, tr_bind' ts)]), dummy_case_term) end
   and imp_monad_bind' bind' return' unit' (const as (c, (_, tys))) ts = if c = bind' then case (ts, tys)
      of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' bind' return' unit' [(t1, ty1), (t2, ty2)]
       | ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' bind' return' unit' [(t1, ty1), (t2, ty2)] `$ t3
       | (ts, _) => imp_monad_bind bind' return' unit' (eta_expand 2 (const, ts))

   and imp_monad_bind bind' return' unit' (IConst const) = imp_monad_bind' bind' return' unit' const []
     | imp_monad_bind bind' return' unit' (t as IVar _) = t
     | imp_monad_bind bind' return' unit' (t as _ `$ _) = (case unfold_app t
        of (IConst const, ts) => imp_monad_bind' bind' return' unit' const ts
         | (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' (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})