tuned
authorhaftmann
Thu Aug 12 08:58:32 2010 +0200 (2010-08-12)
changeset 3838560acf9470a9b
parent 38384 07c33be08476
child 38386 370712dd4628
tuned
src/HOL/Imperative_HOL/Heap_Monad.thy
     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Aug 11 20:25:44 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Aug 12 08:58:32 2010 +0200
     1.3 @@ -536,18 +536,18 @@
     1.4      fun force (t as IConst (c, _) `$ t') = if is_return c
     1.5            then t' else t `$ unitt
     1.6        | force t = t `$ unitt;
     1.7 -    fun tr_bind' [(t1, _), (t2, ty2)] =
     1.8 +    fun tr_bind'' [(t1, _), (t2, ty2)] =
     1.9        let
    1.10          val ((v, ty), t) = dest_abs (t2, ty2);
    1.11 -      in ICase (((force t1, ty), [(IVar v, tr_bind'' t)]), dummy_case_term) end
    1.12 -    and tr_bind'' t = case unfold_app t
    1.13 +      in ICase (((force t1, ty), [(IVar v, tr_bind' t)]), dummy_case_term) end
    1.14 +    and tr_bind' t = case unfold_app t
    1.15           of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if is_bind c
    1.16 -              then tr_bind' [(x1, ty1), (x2, ty2)]
    1.17 +              then tr_bind'' [(x1, ty1), (x2, ty2)]
    1.18                else force t
    1.19            | _ => force t;
    1.20      fun imp_monad_bind'' ts = (SOME dummy_name, unitT) `|=> ICase (((IVar (SOME dummy_name), unitT),
    1.21 -      [(unitt, tr_bind' ts)]), dummy_case_term)
    1.22 -    and imp_monad_bind' (const as (c, (_, tys))) ts = if is_bind c then case (ts, tys)
    1.23 +      [(unitt, tr_bind'' ts)]), dummy_case_term)
    1.24 +    fun 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)]
    1.26          | ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] `$ t3
    1.27          | (ts, _) => imp_monad_bind (eta_expand 2 (const, ts))