src/Tools/eqsubst.ML

--- a/src/Tools/eqsubst.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/Tools/eqsubst.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -179,7 +179,7 @@
 fun fakefree_badbounds Ts t = 
     let val (FakeTs,Ts,newnames) = 
             List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) => 
-                           let val newname = Name.variant usednames n
+                           let val newname = singleton (Name.variant_list usednames) n
                            in ((RWTools.mk_fake_bound_name newname,ty)::FakeTs,
                                (newname,ty)::Ts, 
                                newname::usednames) end)