# HG changeset patch
# User wenzelm
# Date 960069517 -7200
# Node ID 8f75b9ce2f069723c1c10ec0ee95541c72364e28
# Parent  bb7622789bf243ddd48222b9c16d6f60043417f2
fixed Thm.eq_thm: use Sign.joinable;

diff -r bb7622789bf2 -r 8f75b9ce2f06 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sat Jun 03 23:57:40 2000 +0200
+++ b/src/Pure/sign.ML	Sat Jun 03 23:58:37 2000 +0200
@@ -34,6 +34,7 @@
   val deref: sg_ref -> sg
   val self_ref: sg -> sg_ref
   val subsig: sg * sg -> bool
+  val joinable: sg * sg -> bool
   val eq_sg: sg * sg -> bool
   val same_sg: sg * sg -> bool
   val is_draft: sg -> bool
@@ -254,6 +255,8 @@
 end;
 
 
+fun joinable (sg1, sg2) = subsig (sg1, sg2) orelse subsig (sg2, sg1);
+
 (*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*)
diff -r bb7622789bf2 -r 8f75b9ce2f06 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Jun 03 23:57:40 2000 +0200
+++ b/src/Pure/thm.ML	Sat Jun 03 23:58:37 2000 +0200
@@ -426,14 +426,14 @@
 fun apply_attributes (x_th, atts) = Library.apply atts x_th;
 fun applys_attributes (x_ths, atts) = foldl_map (Library.apply atts) x_ths;
 
-(*equality of theorems uses equality of signatures and the
-  a-convertible test for terms*)
 fun eq_thm (th1, th2) =
   let
-    val {sign = sg1, shyps = shyps1, hyps = hyps1, prop = prop1, ...} = rep_thm th1;
-    val {sign = sg2, shyps = shyps2, hyps = hyps2, prop = prop2, ...} = rep_thm th2;
+    val {sign = sg1, shyps = shyps1, hyps = hyps1, prop = prop1, maxidx = _, der = _} =
+      rep_thm th1;
+    val {sign = sg2, shyps = shyps2, hyps = hyps2, prop = prop2, maxidx = _, der = _} =
+      rep_thm th2;
   in
-    Sign.eq_sg (sg1, sg2) andalso
+    Sign.joinable (sg1, sg2) andalso
     eq_set_sort (shyps1, shyps2) andalso
     aconvs (hyps1, hyps2) andalso
     prop1 aconv prop2