adaptated to changes in term representation
authorhaftmann
Tue Jun 30 19:45:52 2009 +0200 (2009-06-30)
changeset 318937d8a89390cbf
parent 31892 a2139b503981
child 31894 bf6207c74448
adaptated to changes in term representation
src/HOL/Imperative_HOL/Heap_Monad.thy
     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Jun 30 19:31:50 2009 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Jun 30 19:45:52 2009 +0200
     1.3 @@ -320,9 +320,9 @@
     1.4        | NONE => K false;
     1.5      val is_bindM = is_const @{const_name bindM};
     1.6      val is_return = is_const @{const_name return};
     1.7 -    val dummy_name = "X";
     1.8 +    val dummy_name = "";
     1.9      val dummy_type = ITyVar dummy_name;
    1.10 -    val dummy_case_term = IVar "";
    1.11 +    val dummy_case_term = IVar NONE;
    1.12      (*assumption: dummy values are not relevant for serialization*)
    1.13      val unitt = case lookup_const naming @{const_name Unity}
    1.14       of SOME unit' => IConst (unit', (([], []), []))
    1.15 @@ -333,7 +333,7 @@
    1.16              val vs = fold_varnames cons t [];
    1.17              val v = Name.variant vs "x";
    1.18              val ty' = (hd o fst o unfold_fun) ty;
    1.19 -          in ((v, ty'), t `$ IVar v) end;
    1.20 +          in ((SOME v, ty'), t `$ IVar (SOME v)) end;
    1.21      fun force (t as IConst (c, _) `$ t') = if is_return c
    1.22            then t' else t `$ unitt
    1.23        | force t = t `$ unitt;
    1.24 @@ -346,7 +346,7 @@
    1.25                then tr_bind' [(x1, ty1), (x2, ty2)]
    1.26                else force t
    1.27            | _ => force t;
    1.28 -    fun imp_monad_bind'' ts = (dummy_name, dummy_type) `|=> ICase (((IVar dummy_name, dummy_type),
    1.29 +    fun imp_monad_bind'' ts = (SOME dummy_name, dummy_type) `|=> ICase (((IVar (SOME dummy_name), dummy_type),
    1.30        [(unitt, tr_bind' ts)]), dummy_case_term)
    1.31      and imp_monad_bind' (const as (c, (_, tys))) ts = if is_bindM c then case (ts, tys)
    1.32         of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)]