--- a/src/Pure/theory.ML Tue Apr 15 18:49:22 2008 +0200
+++ b/src/Pure/theory.ML Tue Apr 15 18:49:23 2008 +0200
@@ -5,16 +5,10 @@
Logical theory content: axioms, definitions, oracles.
*)
-signature BASIC_THEORY =
+signature THEORY =
sig
val eq_thy: theory * theory -> bool
val subthy: theory * theory -> bool
-end
-
-signature THEORY =
-sig
- include BASIC_THEORY
- include SIGN_THEORY
val assert_super: theory -> theory -> theory
val parents_of: theory -> theory list
val ancestors_of: theory -> theory list
@@ -176,12 +170,6 @@
thy |> apply_wrappers (end_wrappers thy) |> Context.finish_thy;
-(* signature operations *)
-
-structure SignTheory: SIGN_THEORY = Sign;
-open SignTheory;
-
-
(** add axioms **)
@@ -346,5 +334,3 @@
end;
-structure BasicTheory: BASIC_THEORY = Theory;
-open BasicTheory;