diff -r 3f31fb81b83a -r 8f3e1ddb50e6 TFL/rules.ML
--- a/TFL/rules.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/TFL/rules.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -513,8 +513,8 @@
             let val eq = Logic.strip_imp_concl body
                 val (f,args) = S.strip_comb (get_lhs eq)
                 val (vstrl,_) = S.strip_abs f
-                val names  = variantlist (map (#1 o dest_Free) vstrl,
-                                          add_term_names(body, []))
+                val names  =
+                  Name.variant_list (add_term_names(body, [])) (map (#1 o dest_Free) vstrl)
             in get (rst, n+1, (names,n)::L) end
             handle TERM _ => get (rst, n+1, L)
               | U.ERR _ => get (rst, n+1, L);