src/HOL/Imperative_HOL/Heap_Monad.thy
changeset 31724 9b5a128cdb5c
parent 31205 98370b26c2ce
child 31871 cc1486840914
     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jun 19 17:23:21 2009 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jun 19 17:26:40 2009 +0200
     1.3 @@ -318,7 +318,7 @@
     1.4        val dummy_case_term = IVar dummy_name;
     1.5        (*assumption: dummy values are not relevant for serialization*)
     1.6        val unitt = IConst (unit', (([], []), []));
     1.7 -      fun dest_abs ((v, ty) `|-> t, _) = ((v, ty), t)
     1.8 +      fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t)
     1.9          | dest_abs (t, ty) =
    1.10              let
    1.11                val vs = Code_Thingol.fold_varnames cons t [];
    1.12 @@ -337,7 +337,7 @@
    1.13                  then tr_bind' [(x1, ty1), (x2, ty2)]
    1.14                  else force t
    1.15              | _ => force t;
    1.16 -    in (dummy_name, dummy_type) `|-> ICase (((IVar dummy_name, dummy_type),
    1.17 +    in (dummy_name, dummy_type) `|=> ICase (((IVar dummy_name, dummy_type),
    1.18        [(unitt, tr_bind' ts)]), dummy_case_term) end
    1.19    and imp_monad_bind' bind' return' unit' (const as (c, (_, tys))) ts = if c = bind' then case (ts, tys)
    1.20       of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' bind' return' unit' [(t1, ty1), (t2, ty2)]
    1.21 @@ -349,7 +349,7 @@
    1.22      | imp_monad_bind bind' return' unit' (t as _ `$ _) = (case unfold_app t
    1.23         of (IConst const, ts) => imp_monad_bind' bind' return' unit' const ts
    1.24          | (t, ts) => imp_monad_bind bind' return' unit' t `$$ map (imp_monad_bind bind' return' unit') ts)
    1.25 -    | imp_monad_bind bind' return' unit' (v_ty `|-> t) = v_ty `|-> imp_monad_bind bind' return' unit' t
    1.26 +    | imp_monad_bind bind' return' unit' (v_ty `|=> t) = v_ty `|=> imp_monad_bind bind' return' unit' t
    1.27      | imp_monad_bind bind' return' unit' (ICase (((t, ty), pats), t0)) = ICase
    1.28          (((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);
    1.29