# HG changeset patch
# User wenzelm
# Date 1020774392 -7200
# Node ID 3d1e7a199bdc7f630b6456a9b5084562eabebee9
# Parent  df7aac8543c92308399338a6fc8cfdf7de938afd
use eq_thm_prop instead of slightly inadequate eq_thm;

diff -r df7aac8543c9 -r 3d1e7a199bdc src/FOLP/simp.ML
--- a/src/FOLP/simp.ML	Tue May 07 14:24:30 2002 +0200
+++ b/src/FOLP/simp.ML	Tue May 07 14:26:32 2002 +0200
@@ -64,7 +64,7 @@
 
 (*** Indexing and filtering of theorems ***)
 
-fun eq_brl ((b1,th1),(b2,th2)) = b1=b2 andalso eq_thm(th1,th2);
+fun eq_brl ((b1,th1),(b2,th2)) = b1=b2 andalso Drule.eq_thm_prop (th1,th2);
 
 (*insert a thm in a discrimination net by its lhs*)
 fun lhs_insert_thm (th,net) =
@@ -247,7 +247,7 @@
 
 (*insert a thm in a thm net*)
 fun insert_thm_warn (th,net) = 
-  Net.insert_term((concl_of th, th), net, eq_thm)
+  Net.insert_term((concl_of th, th), net, Drule.eq_thm_prop)
   handle Net.INSERT => 
     (writeln"\nDuplicate rewrite or congruence rule:"; print_thm th;
      net);
@@ -273,7 +273,7 @@
 
 (*delete a thm from a thm net*)
 fun delete_thm_warn (th,net) = 
-  Net.delete_term((concl_of th, th), net, eq_thm)
+  Net.delete_term((concl_of th, th), net, Drule.eq_thm_prop)
   handle Net.DELETE => 
     (writeln"\nNo such rewrite or congruence rule:";  print_thm th;
      net);
@@ -281,7 +281,7 @@
 val delete_thms = foldr delete_thm_warn;
 
 fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) =
-let val congs' = foldl (gen_rem eq_thm) (congs,thms)
+let val congs' = foldl (gen_rem Drule.eq_thm_prop) (congs,thms)
 in SS{auto_tac=auto_tac, congs= congs',
       cong_net= delete_thms(map mk_trans thms,cong_net),
       mk_simps= normed_rews congs', simps=simps, simp_net=simp_net}
@@ -289,7 +289,7 @@
 
 fun delrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) =
 let fun find((p as (th,ths))::ps',ps) =
-          if eq_thm(thm,th) then (ths,ps@ps') else find(ps',p::ps)
+          if Drule.eq_thm_prop(thm,th) then (ths,ps@ps') else find(ps',p::ps)
       | find([],simps') = (writeln"\nNo such rewrite or congruence rule:";
                            print_thm thm;
                            ([],simps'))
diff -r df7aac8543c9 -r 3d1e7a199bdc src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Tue May 07 14:24:30 2002 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Tue May 07 14:26:32 2002 +0200
@@ -26,7 +26,7 @@
   val empty = Symtab.empty;
   val copy = I;
   val prep_ext = I;
-  val merge = Symtab.merge_multi eq_thm;
+  val merge = Symtab.merge_multi Drule.eq_thm_prop;
   fun print _ _ = ();
 end;
 
diff -r df7aac8543c9 -r 3d1e7a199bdc src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Tue May 07 14:24:30 2002 +0200
+++ b/src/HOL/Tools/meson.ML	Tue May 07 14:26:32 2002 +0200
@@ -266,7 +266,7 @@
 (*Convert a list of clauses to (contrapositive) Horn clauses*)
 fun make_horns ths =
     name_thms "Horn#"
-      (gen_distinct eq_thm (foldr (add_contras clause_rules) (ths,[])));
+      (gen_distinct Drule.eq_thm_prop (foldr (add_contras clause_rules) (ths,[])));
 
 (*Could simply use nprems_of, which would count remaining subgoals -- no
   discrimination as to their size!  With BEST_FIRST, fails for problem 41.*)
diff -r df7aac8543c9 -r 3d1e7a199bdc src/HOL/Tools/recfun_codegen.ML
--- a/src/HOL/Tools/recfun_codegen.ML	Tue May 07 14:24:30 2002 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML	Tue May 07 14:26:32 2002 +0200
@@ -24,7 +24,7 @@
   val empty = Symtab.empty;
   val copy = I;
   val prep_ext = I;
-  val merge = Symtab.merge_multi eq_thm;
+  val merge = Symtab.merge_multi Drule.eq_thm_prop;
   fun print _ _ = ();
 end;
 
diff -r df7aac8543c9 -r 3d1e7a199bdc src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Tue May 07 14:24:30 2002 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Tue May 07 14:26:32 2002 +0200
@@ -107,7 +107,8 @@
              {add_mono_thms= add_mono_thms2, mult_mono_thms= mult_mono_thms2, inj_thms= inj_thms2,
               lessD = lessD2, simpset = simpset2}) =
     {add_mono_thms = Drule.merge_rules (add_mono_thms1, add_mono_thms2),
-     mult_mono_thms = gen_merge_lists' (eq_thm o pairself fst) mult_mono_thms1 mult_mono_thms2,
+     mult_mono_thms = gen_merge_lists' (Drule.eq_thm_prop o pairself fst)
+       mult_mono_thms1 mult_mono_thms2,
      inj_thms = Drule.merge_rules (inj_thms1, inj_thms2),
      lessD = Drule.merge_rules (lessD1, lessD2),
      simpset = Simplifier.merge_ss (simpset1, simpset2)};
diff -r df7aac8543c9 -r 3d1e7a199bdc src/Provers/classical.ML
--- a/src/Provers/classical.ML	Tue May 07 14:24:30 2002 +0200
+++ b/src/Provers/classical.ML	Tue May 07 14:26:32 2002 +0200
@@ -310,8 +310,8 @@
 fun delete x = delete_tagged_list (joinrules x);
 fun delete' x = delete_tagged_list (joinrules' x);
 
-val mem_thm = gen_mem eq_thm
-and rem_thm = gen_rem eq_thm;
+val mem_thm = gen_mem Drule.eq_thm_prop
+and rem_thm = gen_rem Drule.eq_thm_prop;
 
 (*Warn if the rule is already present ELSEWHERE in the claset.  The addition
   is still allowed.*)
@@ -601,10 +601,10 @@
   treatment of priority might get muddled up.*)
 fun merge_cs (cs as CS{safeIs, safeEs, hazIs, hazEs, ...},
      CS{safeIs=safeIs2, safeEs=safeEs2, hazIs=hazIs2, hazEs=hazEs2, swrappers, uwrappers, ...}) =
-  let val safeIs' = gen_rems eq_thm (safeIs2,safeIs)
-      val safeEs' = gen_rems eq_thm (safeEs2,safeEs)
-      val  hazIs' = gen_rems eq_thm ( hazIs2, hazIs)
-      val  hazEs' = gen_rems eq_thm ( hazEs2, hazEs)
+  let val safeIs' = gen_rems Drule.eq_thm_prop (safeIs2,safeIs)
+      val safeEs' = gen_rems Drule.eq_thm_prop (safeEs2,safeEs)
+      val hazIs' = gen_rems Drule.eq_thm_prop (hazIs2, hazIs)
+      val hazEs' = gen_rems Drule.eq_thm_prop (hazEs2, hazEs)
       val cs1   = cs addSIs safeIs'
                      addSEs safeEs'
                      addIs  hazIs'
diff -r df7aac8543c9 -r 3d1e7a199bdc src/Provers/induct_method.ML
--- a/src/Provers/induct_method.ML	Tue May 07 14:24:30 2002 +0200
+++ b/src/Provers/induct_method.ML	Tue May 07 14:26:32 2002 +0200
@@ -260,7 +260,7 @@
     val sg = ProofContext.sign_of ctxt;
     val cert = Thm.cterm_of sg;
 
-    fun rule_versions r = Seq.cons (r, Seq.filter (not o curry eq_thm r)
+    fun rule_versions r = Seq.cons (r, Seq.filter (not o curry Thm.eq_thm r)
         (Seq.make (fn () => Some (localize r, Seq.empty))))
       |> Seq.map (rpair (RuleCases.get r));
 
diff -r df7aac8543c9 -r 3d1e7a199bdc src/Provers/simp.ML
--- a/src/Provers/simp.ML	Tue May 07 14:24:30 2002 +0200
+++ b/src/Provers/simp.ML	Tue May 07 14:26:32 2002 +0200
@@ -58,7 +58,7 @@
 
 (*** Indexing and filtering of theorems ***)
 
-fun eq_brl ((b1,th1),(b2,th2)) = b1=b2 andalso eq_thm(th1,th2);
+fun eq_brl ((b1,th1),(b2,th2)) = b1=b2 andalso Drule.eq_thm_prop(th1,th2);
 
 (*insert a thm in a discrimination net by its lhs*)
 fun lhs_insert_thm (th,net) =
@@ -244,7 +244,7 @@
 
 (*insert a thm in a thm net*)
 fun insert_thm_warn (th,net) = 
-  Net.insert_term((concl_of th, th), net, eq_thm)
+  Net.insert_term((concl_of th, th), net, Drule.eq_thm_prop)
   handle Net.INSERT => 
     (writeln"\nDuplicate rewrite or congruence rule:"; print_thm th;
      net);
@@ -289,7 +289,7 @@
 
 (*delete a thm from a thm net*)
 fun delete_thm_warn (th,net) = 
-  Net.delete_term((concl_of th, th), net, eq_thm)
+  Net.delete_term((concl_of th, th), net, Drule.eq_thm_prop)
   handle Net.DELETE => 
     (writeln"\nNo such rewrite or congruence rule:";  print_thm th;
      net);
@@ -298,7 +298,7 @@
 
 fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net,
                    splits,split_consts}, thms) =
-let val congs' = foldl (gen_rem eq_thm) (congs,thms)
+let val congs' = foldl (gen_rem Drule.eq_thm_prop) (congs,thms)
 in SS{auto_tac=auto_tac, congs= congs',
       cong_net= delete_thms(map mk_trans thms,cong_net),
       mk_simps= normed_rews congs', simps=simps, simp_net=simp_net,
@@ -308,7 +308,7 @@
 fun delrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net,
               splits,split_consts}, thm) =
 let fun find((p as (th,ths))::ps',ps) =
-	  if eq_thm(thm,th) then (ths,ps@ps') else find(ps',p::ps)
+	  if Drule.eq_thm_prop(thm,th) then (ths,ps@ps') else find(ps',p::ps)
       | find([],simps') = (writeln"\nNo such rewrite or congruence rule:";
 			   print_thm thm;
 			   ([],simps'))
diff -r df7aac8543c9 -r 3d1e7a199bdc src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Tue May 07 14:24:30 2002 +0200
+++ b/src/Pure/Isar/context_rules.ML	Tue May 07 14:26:32 2002 +0200
@@ -103,7 +103,7 @@
 
 fun del_rule th (rs as Rules {next, rules, netpairs, wrappers}) =
   let
-    fun eq_th (_, (_, th')) = Thm.eq_thm (th, th');
+    fun eq_th (_, (_, th')) = Drule.eq_thm_prop (th, th');
     fun del b netpair = delete_tagged_brl ((b, th), netpair) handle Net.DELETE => netpair;
   in
     if not (exists eq_th rules) then rs
@@ -135,7 +135,7 @@
     let
       val wrappers = (gen_merge_lists' eq_snd ws1 ws2, gen_merge_lists' eq_snd ws1' ws2');
       val rules = gen_merge_lists' (fn ((_, (k1, th1)), (_, (k2, th2))) =>
-          k1 = k2 andalso Thm.eq_thm (th1, th2)) rules1 rules2;
+          k1 = k2 andalso Drule.eq_thm_prop (th1, th2)) rules1 rules2;
       val next = ~ (length rules);
       val netpairs = foldl (fn (nps, (n, (w, ((i, b), th)))) =>
           map_nth_elem i (curry insert_tagged_brl ((w, n), (b, th))) nps)
diff -r df7aac8543c9 -r 3d1e7a199bdc src/Pure/Isar/induct_attrib.ML
--- a/src/Pure/Isar/induct_attrib.ML	Tue May 07 14:24:30 2002 +0200
+++ b/src/Pure/Isar/induct_attrib.ML	Tue May 07 14:26:32 2002 +0200
@@ -84,7 +84,8 @@
 type rules = (string * thm) NetRules.T;
 
 val init_rules =
-  NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso Thm.eq_thm (th1, th2));
+  NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso
+    Drule.eq_thm_prop (th1, th2));
 
 fun lookup_rule (rs: rules) name = Library.assoc (NetRules.rules rs, name);
 
diff -r df7aac8543c9 -r 3d1e7a199bdc src/Pure/Isar/net_rules.ML
--- a/src/Pure/Isar/net_rules.ML	Tue May 07 14:24:30 2002 +0200
+++ b/src/Pure/Isar/net_rules.ML	Tue May 07 14:26:32 2002 +0200
@@ -63,8 +63,8 @@
 
 (* intro/elim rules *)
 
-val intro = init Thm.eq_thm Thm.concl_of;
-val elim = init Thm.eq_thm Thm.major_prem_of;
+val intro = init Drule.eq_thm_prop Thm.concl_of;
+val elim = init Drule.eq_thm_prop Thm.major_prem_of;
 
 
 end;
diff -r df7aac8543c9 -r 3d1e7a199bdc src/Pure/drule.ML
--- a/src/Pure/drule.ML	Tue May 07 14:24:30 2002 +0200
+++ b/src/Pure/drule.ML	Tue May 07 14:26:32 2002 +0200
@@ -55,8 +55,9 @@
   val read_instantiate_sg: Sign.sg -> (string*string)list -> thm -> thm
   val read_instantiate  : (string*string)list -> thm -> thm
   val cterm_instantiate : (cterm*cterm)list -> thm -> thm
+  val eq_thm_sg         : thm * thm -> bool
+  val eq_thm_prop	: thm * thm -> bool
   val weak_eq_thm       : thm * thm -> bool
-  val eq_thm_sg         : thm * thm -> bool
   val size_of_thm       : thm -> int
   val reflexive_thm     : thm
   val symmetric_thm     : thm
@@ -490,20 +491,21 @@
         [th] => th
       | _ =>   raise THM("COMP", 1, [tha,thb]);
 
+
 (** theorem equality **)
 
-(*Do the two theorems have the same signature?*)
-fun eq_thm_sg (th1,th2) = Sign.eq_sg(#sign(rep_thm th1), #sign(rep_thm th2));
+val eq_thm_sg = Sign.eq_sg o pairself Thm.sign_of_thm;
+val eq_thm_prop = op aconv o pairself Thm.prop_of;
 
 (*Useful "distance" function for BEST_FIRST*)
 val size_of_thm = size_of_term o prop_of;
 
 (*maintain lists of theorems --- preserving canonical order*)
-fun del_rules rs rules = Library.gen_rems Thm.eq_thm (rules, rs);
+fun del_rules rs rules = Library.gen_rems eq_thm_prop (rules, rs);
 fun add_rules rs rules = rs @ del_rules rs rules;
 val del_rule = del_rules o single;
 val add_rule = add_rules o single;
-fun merge_rules (rules1, rules2) = gen_merge_lists' Thm.eq_thm rules1 rules2;
+fun merge_rules (rules1, rules2) = gen_merge_lists' eq_thm_prop rules1 rules2;
 
 
 (** Mark Staples's weaker version of eq_thm: ignores variable renaming and
@@ -522,9 +524,7 @@
       val vars = distinct (term_vars' prop);
   in forall_intr_list (map (cterm_of sign) vars) th end;
 
-fun weak_eq_thm (tha,thb) =
-    eq_thm(forall_intr_vars (freezeT tha), forall_intr_vars (freezeT thb));
-
+val weak_eq_thm = Thm.eq_thm o pairself (forall_intr_vars o freezeT);
 
 
 (*** Meta-Rewriting Rules ***)
diff -r df7aac8543c9 -r 3d1e7a199bdc src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Tue May 07 14:24:30 2002 +0200
+++ b/src/Pure/tactic.ML	Tue May 07 14:26:32 2002 +0200
@@ -410,7 +410,7 @@
 
 (*delete one kbrl from the pair of nets*)
 local
-  fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = eq_thm (th, th')
+  fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Drule.eq_thm_prop (th, th')
 in
 fun delete_tagged_brl (brl as (eres, th), (inet, enet)) =
   if eres then
diff -r df7aac8543c9 -r 3d1e7a199bdc src/Sequents/prover.ML
--- a/src/Sequents/prover.ML	Tue May 07 14:24:30 2002 +0200
+++ b/src/Sequents/prover.ML	Tue May 07 14:26:32 2002 +0200
@@ -32,15 +32,15 @@
        dups);
 
 fun (Pack(safes,unsafes)) add_safes ths   = 
-    let val dups = warn_duplicates (gen_inter eq_thm (ths,safes))
-	val ths' = gen_rems eq_thm (ths,dups)
+    let val dups = warn_duplicates (gen_inter Drule.eq_thm_prop (ths,safes))
+	val ths' = gen_rems Drule.eq_thm_prop (ths,dups)
     in
         Pack(sort (make_ord less) (ths'@safes), unsafes)
     end;
 
 fun (Pack(safes,unsafes)) add_unsafes ths = 
-    let val dups = warn_duplicates (gen_inter eq_thm (ths,unsafes))
-	val ths' = gen_rems eq_thm (ths,dups)
+    let val dups = warn_duplicates (gen_inter Drule.eq_thm_prop (ths,unsafes))
+	val ths' = gen_rems Drule.eq_thm_prop (ths,dups)
     in
 	Pack(safes, sort (make_ord less) (ths'@unsafes))
     end;
diff -r df7aac8543c9 -r 3d1e7a199bdc src/ZF/Tools/typechk.ML
--- a/src/ZF/Tools/typechk.ML	Tue May 07 14:24:30 2002 +0200
+++ b/src/ZF/Tools/typechk.ML	Tue May 07 14:26:32 2002 +0200
@@ -46,8 +46,8 @@
            net: thm Net.net};   (*discrimination net of the same rules*)
 
 
-val mem_thm = gen_mem eq_thm
-and rem_thm = gen_rem eq_thm;
+val mem_thm = gen_mem Drule.eq_thm_prop
+and rem_thm = gen_rem Drule.eq_thm_prop;
 
 fun addTC (cs as TC{rules, net}, th) =
   if mem_thm (th, rules) then
@@ -61,7 +61,7 @@
 
 fun delTC (cs as TC{rules, net}, th) =
   if mem_thm (th, rules) then
-      TC{net = Net.delete_term ((concl_of th, th), net, eq_thm),
+      TC{net = Net.delete_term ((concl_of th, th), net, Drule.eq_thm_prop),
          rules  = rem_thm (rules,th)}
   else (warning ("No such type-checking rule\n" ^ (string_of_thm th));
         cs);
@@ -110,8 +110,8 @@
 
 
 fun merge_tc (TC{rules,net}, TC{rules=rules',net=net'}) =
-    TC {rules = gen_union eq_thm (rules,rules'),
-        net = Net.merge (net, net', eq_thm)};
+    TC {rules = gen_union Drule.eq_thm_prop (rules,rules'),
+        net = Net.merge (net, net', Drule.eq_thm_prop)};
 
 (*print tcsets*)
 fun print_tc (TC{rules,...}) =