src/Provers/eqsubst.ML

--- a/src/Provers/eqsubst.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/src/Provers/eqsubst.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -180,7 +180,7 @@
 fun fakefree_badbounds Ts t = 
     let val (FakeTs,Ts,newnames) = 
             List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) => 
-                           let val newname = Term.variant usednames n
+                           let val newname = Name.variant usednames n
                            in ((RWTools.mk_fake_bound_name newname,ty)::FakeTs,
                                (newname,ty)::Ts, 
                                newname::usednames) end)