1.1 --- a/src/Pure/drule.ML	Tue May 07 14:24:30 2002 +0200
     1.2 +++ b/src/Pure/drule.ML	Tue May 07 14:26:32 2002 +0200
     1.3 @@ -55,8 +55,9 @@
     1.4    val read_instantiate_sg: Sign.sg -> (string*string)list -> thm -> thm
     1.5    val read_instantiate  : (string*string)list -> thm -> thm
     1.6    val cterm_instantiate : (cterm*cterm)list -> thm -> thm
     1.7 +  val eq_thm_sg         : thm * thm -> bool
     1.8 +  val eq_thm_prop	: thm * thm -> bool
     1.9    val weak_eq_thm       : thm * thm -> bool
    1.10 -  val eq_thm_sg         : thm * thm -> bool
    1.11    val size_of_thm       : thm -> int
    1.12    val reflexive_thm     : thm
    1.13    val symmetric_thm     : thm
    1.14 @@ -490,20 +491,21 @@
    1.15          [th] => th
    1.16        | _ =>   raise THM("COMP", 1, [tha,thb]);
    1.17  
    1.18 +
    1.19  (** theorem equality **)
    1.20  
    1.21 -(*Do the two theorems have the same signature?*)
    1.22 -fun eq_thm_sg (th1,th2) = Sign.eq_sg(#sign(rep_thm th1), #sign(rep_thm th2));
    1.23 +val eq_thm_sg = Sign.eq_sg o pairself Thm.sign_of_thm;
    1.24 +val eq_thm_prop = op aconv o pairself Thm.prop_of;
    1.25  
    1.26  (*Useful "distance" function for BEST_FIRST*)
    1.27  val size_of_thm = size_of_term o prop_of;
    1.28  
    1.29  (*maintain lists of theorems --- preserving canonical order*)
    1.30 -fun del_rules rs rules = Library.gen_rems Thm.eq_thm (rules, rs);
    1.31 +fun del_rules rs rules = Library.gen_rems eq_thm_prop (rules, rs);
    1.32  fun add_rules rs rules = rs @ del_rules rs rules;
    1.33  val del_rule = del_rules o single;
    1.34  val add_rule = add_rules o single;
    1.35 -fun merge_rules (rules1, rules2) = gen_merge_lists' Thm.eq_thm rules1 rules2;
    1.36 +fun merge_rules (rules1, rules2) = gen_merge_lists' eq_thm_prop rules1 rules2;
    1.37  
    1.38  
    1.39  (** Mark Staples's weaker version of eq_thm: ignores variable renaming and
    1.40 @@ -522,9 +524,7 @@
    1.41        val vars = distinct (term_vars' prop);
    1.42    in forall_intr_list (map (cterm_of sign) vars) th end;
    1.43  
    1.44 -fun weak_eq_thm (tha,thb) =
    1.45 -    eq_thm(forall_intr_vars (freezeT tha), forall_intr_vars (freezeT thb));
    1.46 -
    1.47 +val weak_eq_thm = Thm.eq_thm o pairself (forall_intr_vars o freezeT);
    1.48  
    1.49  
    1.50  (*** Meta-Rewriting Rules ***)