# HG changeset patch
# User wenzelm
# Date 1120050803 -7200
# Node ID 5d73fbf4eb1e93e71e1cdc4a48455c85f66483e4
# Parent  0115764233e4ec2b79195106e18a857033962dae
added joinable;

diff -r 0115764233e4 -r 5d73fbf4eb1e src/Pure/context.ML
--- 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 *)