--- a/src/Pure/context.ML Tue Jun 28 17:56:04 2005 +0200
+++ b/src/Pure/context.ML Wed Jun 29 15:13:23 2005 +0200
@@ -39,6 +39,7 @@
val check_thy: string -> theory -> theory
val eq_thy: theory * theory -> bool
val subthy: theory * theory -> bool
+ val joinable: theory * theory -> bool
val merge: theory * theory -> theory (*exception TERM*)
val merge_refs: theory_ref * theory_ref -> theory_ref (*exception TERM*)
val self_ref: theory -> theory_ref
@@ -279,6 +280,8 @@
fun subthy thys = eq_thy thys orelse proper_subthy thys;
+fun joinable (thy1, thy2) = subthy (thy1, thy2) orelse subthy (thy2, thy1);
+
(* theory references *)