removed obsolete SIGN_THEORY -- no name aliases in structure Theory;
authorwenzelm
Tue Apr 15 18:49:23 2008 +0200 (2008-04-15)
changeset 2666865023d4fd226
parent 26667 660b69b3c28a
child 26669 c27efd6de25d
removed obsolete SIGN_THEORY -- no name aliases in structure Theory;
removed obsolete BASIC_THEORY;
src/Pure/theory.ML
     1.1 --- a/src/Pure/theory.ML	Tue Apr 15 18:49:22 2008 +0200
     1.2 +++ b/src/Pure/theory.ML	Tue Apr 15 18:49:23 2008 +0200
     1.3 @@ -5,16 +5,10 @@
     1.4  Logical theory content: axioms, definitions, oracles.
     1.5  *)
     1.6  
     1.7 -signature BASIC_THEORY =
     1.8 +signature THEORY =
     1.9  sig
    1.10    val eq_thy: theory * theory -> bool
    1.11    val subthy: theory * theory -> bool
    1.12 -end
    1.13 -
    1.14 -signature THEORY =
    1.15 -sig
    1.16 -  include BASIC_THEORY
    1.17 -  include SIGN_THEORY
    1.18    val assert_super: theory -> theory -> theory
    1.19    val parents_of: theory -> theory list
    1.20    val ancestors_of: theory -> theory list
    1.21 @@ -176,12 +170,6 @@
    1.22    thy |> apply_wrappers (end_wrappers thy) |> Context.finish_thy;
    1.23  
    1.24  
    1.25 -(* signature operations *)
    1.26 -
    1.27 -structure SignTheory: SIGN_THEORY = Sign;
    1.28 -open SignTheory;
    1.29 -
    1.30 -
    1.31  
    1.32  (** add axioms **)
    1.33  
    1.34 @@ -346,5 +334,3 @@
    1.35  
    1.36  end;
    1.37  
    1.38 -structure BasicTheory: BASIC_THEORY = Theory;
    1.39 -open BasicTheory;