src/HOL/Imperative_HOL/Heap_Monad.thy
changeset 43324 2b47822868e4
parent 43080 73a1d6a7ef1d
child 44174 d1d79f0e1ea6
     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Jun 09 15:38:49 2011 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Jun 09 16:34:49 2011 +0200
     1.3 @@ -618,7 +618,6 @@
     1.4  open Code_Thingol;
     1.5  
     1.6  fun imp_program naming =
     1.7 -
     1.8    let
     1.9      fun is_const c = case lookup_const naming c
    1.10       of SOME c' => (fn c'' => c' = c'')
    1.11 @@ -635,7 +634,7 @@
    1.12        | dest_abs (t, ty) =
    1.13            let
    1.14              val vs = fold_varnames cons t [];
    1.15 -            val v = Name.variant vs "x";
    1.16 +            val v = singleton (Name.variant_list vs) "x";
    1.17              val ty' = (hd o fst o unfold_fun) ty;
    1.18            in ((SOME v, ty'), t `$ IVar (SOME v)) end;
    1.19      fun force (t as IConst (c, _) `$ t') = if is_return c