diff -r d5f7b424ba47 -r b710a5087116 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Sun Aug 16 17:11:31 2015 +0200
+++ b/src/Pure/theory.ML	Sun Aug 16 18:19:30 2015 +0200
@@ -6,8 +6,6 @@
 
 signature THEORY =
 sig
-  val eq_thy: theory * theory -> bool
-  val subthy: theory * theory -> bool
   val parents_of: theory -> theory list
   val ancestors_of: theory -> theory list
   val nodes_of: theory -> theory list
@@ -40,9 +38,6 @@
 
 (** theory context operations **)
 
-val eq_thy = Context.eq_thy;
-val subthy = Context.subthy;
-
 val parents_of = Context.parents_of;
 val ancestors_of = Context.ancestors_of;
 fun nodes_of thy = thy :: ancestors_of thy;