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 *)