src/HOL/Imperative_HOL/Heap_Monad.thy

 let
 
 open Code_Thingol;
 
 fun imp_program naming =
-
   let
     fun is_const c = case lookup_const naming c
      of SOME c' => (fn c'' => c' = c'')
       | NONE => K false;
     val is_bind = is_const @{const_name bind};

       | NONE => error ("Must include " ^ @{const_name Unity} ^ " in generated constants.");
     fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t)
       | 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
           then t' else t `$ unitt
       | force t = t `$ unitt;