# HG changeset patch
# User clasohm
# Date 809954868 -7200
# Node ID bfc93c86f0a147100559e99cc5bd58486485c604
# Parent  0901441a7ebf967492a75cc129f8c8a9ac7e2dd5
added same_sg and same_thm

diff -r 0901441a7ebf -r bfc93c86f0a1 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Fri Sep 01 13:16:24 1995 +0200
+++ b/src/Pure/drule.ML	Fri Sep 01 13:27:48 1995 +0200
@@ -26,6 +26,7 @@
   val equal_abs_elim	: cterm  -> thm -> thm
   val equal_abs_elim_list: cterm list -> thm -> thm
   val eq_thm		: thm * thm -> bool
+  val same_thm		: thm * thm -> bool
   val eq_thm_sg		: thm * thm -> bool
   val flexpair_abs_elim_list: cterm list -> thm -> thm
   val forall_intr_list	: cterm list -> thm -> thm
@@ -648,6 +649,18 @@
         prop1 aconv prop2
     end;
 
+(*equality of theorems using similarity of signatures,
+  i.e. the theorems belong to the same theory but not necessarily to the same
+  version of this theory*)
+fun same_thm (th1,th2) =
+    let val {sign=sg1, shyps=shyps1, hyps=hyps1, prop=prop1, ...} = rep_thm th1
+        and {sign=sg2, shyps=shyps2, hyps=hyps2, prop=prop2, ...} = rep_thm th2
+    in  Sign.same_sg (sg1,sg2) andalso
+        eq_set (shyps1, shyps2) andalso
+        aconvs(hyps1,hyps2) andalso
+        prop1 aconv prop2
+    end;
+
 (*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));
 
diff -r 0901441a7ebf -r bfc93c86f0a1 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Fri Sep 01 13:16:24 1995 +0200
+++ b/src/Pure/sign.ML	Fri Sep 01 13:27:48 1995 +0200
@@ -20,6 +20,7 @@
        stamps: string ref list}
     val subsig: sg * sg -> bool
     val eq_sg: sg * sg -> bool
+    val same_sg: sg * sg -> bool
     val is_draft: sg -> bool
     val const_type: sg -> string -> typ option
     val classes: sg -> class list
@@ -107,6 +108,12 @@
 
 fun eq_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) = eq_set (s1, s2);
 
+(* test if same theory names are contained in signatures' stamps,
+   i.e. if signatures belong to same theory but not necessarily to the same
+   version of it*)
+fun same_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) =
+  eq_set (pairself (map (op !)) (s1, s2));
+
 
 (* consts *)