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