src/Pure/sign.ML

   val stamp_names_of: sg -> string list
   val tsig_of: sg -> Type.type_sig
   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
   val is_stale: sg -> bool
   val const_type: sg -> string -> typ option

   fun fast_subsig (sg1 as Sg ({stamps = s1, ...}, _), sg2 as Sg ({stamps = s2, ...}, _)) =
     eq_sg (sg1, sg2) orelse fast_sub (s1, s2);
 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*)
 fun same_sg (sg1 as Sg ({stamps = s1, ...}, _), sg2 as Sg ({stamps = s2, ...}, _)) =
   eq_sg (sg1, sg2) orelse eq_set_string (pairself (map (op !)) (s1, s2));