diff -r 981fa0ce23ed -r 868120282837 TFL/rules.ML
--- a/TFL/rules.ML	Tue Oct 10 13:59:12 2006 +0200
+++ b/TFL/rules.ML	Tue Oct 10 13:59:13 2006 +0200
@@ -763,8 +763,8 @@
               val dummy = print_thms "cntxt:" cntxt
               val {prop = Const("==>",_) $ (Const("Trueprop",_) $ A) $ _,
                    sign,...} = rep_thm thm
-              fun genl tm = let val vlist = gen_rems (op aconv)
-                                           (add_term_frees(tm,[]), globals)
+              fun genl tm = let val vlist = subtract (op aconv) globals
+                                           (add_term_frees(tm,[]))
                             in fold_rev Forall vlist tm
                             end
               (*--------------------------------------------------------------