--- a/src/HOL/Tools/Predicate_Compile/mode_inference.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/mode_inference.ML Thu Jun 09 16:34:49 2011 +0200
@@ -249,7 +249,7 @@
end
else
let
- val s = Name.variant names "x"
+ val s = singleton (Name.variant_list names) "x"
val v = Free (s, fastype_of t)
in
(v, (s :: names, HOLogic.mk_eq (v, t) :: eqs))
@@ -257,7 +257,7 @@
(*
if is_constrt thy t then (t, (names, eqs)) else
let
- val s = Name.variant names "x"
+ val s = singleton (Name.variant_list names) "x"
val v = Free (s, fastype_of t)
in (v, (s::names, HOLogic.mk_eq (v, t)::eqs)) end;
*)