--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Thu Jun 09 16:34:49 2011 +0200
@@ -618,7 +618,6 @@
open Code_Thingol;
fun imp_program naming =
-
let
fun is_const c = case lookup_const naming c
of SOME c' => (fn c'' => c' = c'')
@@ -635,7 +634,7 @@
| dest_abs (t, ty) =
let
val vs = fold_varnames cons t [];
- val v = Name.variant vs "x";
+ val v = singleton (Name.variant_list vs) "x";
val ty' = (hd o fst o unfold_fun) ty;
in ((SOME v, ty'), t `$ IVar (SOME v)) end;
fun force (t as IConst (c, _) `$ t') = if is_return c