# HG changeset patch
# User wenzelm
# Date 1208278163 -7200
# Node ID 65023d4fd226a7b09a8d8648e932816360206440
# Parent  660b69b3c28a09d9f888d3afd6a96f58f032b705
removed obsolete SIGN_THEORY -- no name aliases in structure Theory;
removed obsolete BASIC_THEORY;

diff -r 660b69b3c28a -r 65023d4fd226 src/Pure/theory.ML
--- 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;