src/Pure/theory.ML

 Logical theory content: axioms, definitions, oracles.
 *)
 
 signature BASIC_THEORY =
 sig
-  type theory
-  type theory_ref
   val sign_of: theory -> theory    (*obsolete*)
   val rep_theory: theory ->
    {axioms: term NameSpace.table,
     defs: Defs.T,
     oracles: ((theory * Object.T -> term) * stamp) NameSpace.table}

 
 (** type theory **)
 
 (* context operations *)
 
-type theory = Context.theory;
-type theory_ref = Context.theory_ref;
-
 val eq_thy = Context.eq_thy;
 val subthy = Context.subthy;
 
 val parents_of = Context.parents_of;
 val ancestors_of = Context.ancestors_of;