--- a/src/Pure/context.ML Mon Feb 17 21:37:41 2014 +0100
+++ b/src/Pure/context.ML Mon Feb 17 22:39:20 2014 +0100
@@ -43,7 +43,6 @@
val this_theory: theory -> string -> theory
val eq_thy: theory * theory -> bool
val subthy: theory * theory -> bool
- val joinable: theory * theory -> bool
val merge: theory * theory -> theory
val finish_thy: theory -> theory
val begin_thy: (theory -> pretty) -> string -> theory list -> theory
@@ -246,8 +245,6 @@
fun subthy thys = eq_thy thys orelse proper_subthy thys;
-fun joinable (thy1, thy2) = subthy (thy1, thy2) orelse subthy (thy2, thy1);
-
(* consistent ancestors *)