TFL/rules.new.sml

     Copyright   1997  University of Cambridge
 
 Emulation of HOL inference rules for TFL
 *)
 
-structure FastRules : Rules_sig = 
+structure Rules : Rules_sig = 
 struct
 
 open Utils;
 
 structure USyntax  = USyntax;
 structure S  = USyntax;
 structure U  = Utils;
 structure D = Dcterm;
 
 
-fun RULES_ERR{func,mesg} = Utils.ERR{module = "FastRules",func=func,mesg=mesg};
+fun RULES_ERR{func,mesg} = Utils.ERR{module = "Rules",func=func,mesg=mesg};
 
 
 fun cconcl thm = D.drop_prop(#prop(crep_thm thm));
 fun chyps thm = map D.drop_prop(#hyps(crep_thm thm));
 

          | (vlist,body) =>
             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  = map (#1 o dest_Free)
-                                 (variants (S.free_vars body) vstrl)
+                                 (variants (term_frees body) vstrl)
             in get (rst, n+1, (names,n)::L)
             end handle _ => get (rst, n+1, L);
 
 (* Note: rename_params_rule counts from 1, not 0 *)
 fun rename thm = 

           let val dummy = say "restrict_prover:\n"
               val cntxt = rev(prems_of_mss mss)
               val dummy = print_thms "cntxt:\n" cntxt
               val {prop = Const("==>",_) $ (Const("Trueprop",_) $ A) $ _,
                    sign,...} = rep_thm thm
-              fun genl tm = let val vlist = U.set_diff (curry(op aconv))
-                                           (add_term_frees(tm,[])) [func,R]
+              fun genl tm = let val vlist = gen_rems (op aconv)
+                                           (add_term_frees(tm,[]), [func,R])
                             in U.itlist Forall vlist tm
                             end
               (*--------------------------------------------------------------
                * This actually isn't quite right, since it will think that
                * not-fully applied occs. of "f" in the context mean that the