--- 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;