--- a/src/Pure/theory.ML Mon Oct 13 22:43:29 2014 +0200
+++ b/src/Pure/theory.ML Tue Oct 14 10:52:46 2014 +0200
@@ -8,7 +8,6 @@
sig
val eq_thy: theory * theory -> bool
val subthy: theory * theory -> bool
- val assert_super: theory -> theory -> theory
val parents_of: theory -> theory list
val ancestors_of: theory -> theory list
val nodes_of: theory -> theory list
@@ -43,10 +42,6 @@
val eq_thy = Context.eq_thy;
val subthy = Context.subthy;
-fun assert_super thy1 thy2 =
- if subthy (thy1, thy2) then thy2
- else raise THEORY ("Not a super theory", [thy1, thy2]);
-
val parents_of = Context.parents_of;
val ancestors_of = Context.ancestors_of;
fun nodes_of thy = thy :: ancestors_of thy;