1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Jul 28 14:11:48 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Jul 29 09:56:59 2010 +0200
     1.3 @@ -521,11 +521,10 @@
     1.4      val is_bind = is_const @{const_name bind};
     1.5      val is_return = is_const @{const_name return};
     1.6      val dummy_name = "";
     1.7 -    val dummy_type = ITyVar dummy_name;
     1.8      val dummy_case_term = IVar NONE;
     1.9      (*assumption: dummy values are not relevant for serialization*)
    1.10 -    val unitt = case lookup_const naming @{const_name Unity}
    1.11 -     of SOME unit' => IConst (unit', (([], []), []))
    1.12 +    val (unitt, unitT) = case lookup_const naming @{const_name Unity}
    1.13 +     of SOME unit' => (IConst (unit', (([], []), [])), the (lookup_tyco naming @{type_name unit}) `%% [])
    1.14        | NONE => error ("Must include " ^ @{const_name Unity} ^ " in generated constants.");
    1.15      fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t)
    1.16        | dest_abs (t, ty) =
    1.17 @@ -546,7 +545,7 @@
    1.18                then tr_bind' [(x1, ty1), (x2, ty2)]
    1.19                else force t
    1.20            | _ => force t;
    1.21 -    fun imp_monad_bind'' ts = (SOME dummy_name, dummy_type) `|=> ICase (((IVar (SOME dummy_name), dummy_type),
    1.22 +    fun imp_monad_bind'' ts = (SOME dummy_name, unitT) `|=> ICase (((IVar (SOME dummy_name), unitT),
    1.23        [(unitt, tr_bind' ts)]), dummy_case_term)
    1.24      and imp_monad_bind' (const as (c, (_, tys))) ts = if is_bind c then case (ts, tys)
    1.25         of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)]