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