src/HOL/Imperative_HOL/Heap_Monad.thy
changeset 31058 9f151b096533
parent 29793 86cac1fab613
child 31205 98370b26c2ce
     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed May 06 19:42:27 2009 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu May 07 12:02:15 2009 +0200
     1.3 @@ -317,7 +317,7 @@
     1.4        val dummy_type = ITyVar dummy_name;
     1.5        val dummy_case_term = IVar dummy_name;
     1.6        (*assumption: dummy values are not relevant for serialization*)
     1.7 -      val unitt = IConst (unit', ([], []));
     1.8 +      val unitt = IConst (unit', (([], []), []));
     1.9        fun dest_abs ((v, ty) `|-> t, _) = ((v, ty), t)
    1.10          | dest_abs (t, ty) =
    1.11              let
    1.12 @@ -353,10 +353,10 @@
    1.13      | imp_monad_bind bind' return' unit' (ICase (((t, ty), pats), t0)) = ICase
    1.14          (((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.15  
    1.16 -   fun imp_program naming = (Graph.map_nodes o map_terms_stmt)
    1.17 -     (imp_monad_bind (lookup naming @{const_name bindM})
    1.18 -       (lookup naming @{const_name return})
    1.19 -       (lookup naming @{const_name Unity}));
    1.20 +  fun imp_program naming = (Graph.map_nodes o map_terms_stmt)
    1.21 +    (imp_monad_bind (lookup naming @{const_name bindM})
    1.22 +      (lookup naming @{const_name return})
    1.23 +      (lookup naming @{const_name Unity}));
    1.24  
    1.25  in
    1.26