src/Pure/theory.ML
changeset 20549 c643984eb94b
parent 20392 88cab786d024
child 21608 2ca27eeb2841
     1.1 --- a/src/Pure/theory.ML	Fri Sep 15 22:56:13 2006 +0200
     1.2 +++ b/src/Pure/theory.ML	Fri Sep 15 22:56:17 2006 +0200
     1.3 @@ -7,8 +7,6 @@
     1.4  
     1.5  signature BASIC_THEORY =
     1.6  sig
     1.7 -  type theory
     1.8 -  type theory_ref
     1.9    val sign_of: theory -> theory    (*obsolete*)
    1.10    val rep_theory: theory ->
    1.11     {axioms: term NameSpace.table,
    1.12 @@ -63,9 +61,6 @@
    1.13  
    1.14  (* context operations *)
    1.15  
    1.16 -type theory = Context.theory;
    1.17 -type theory_ref = Context.theory_ref;
    1.18 -
    1.19  val eq_thy = Context.eq_thy;
    1.20  val subthy = Context.subthy;
    1.21