src/Pure/theory.ML
changeset 20549 c643984eb94b
parent 20392 88cab786d024
child 21608 2ca27eeb2841
--- a/src/Pure/theory.ML	Fri Sep 15 22:56:13 2006 +0200
+++ b/src/Pure/theory.ML	Fri Sep 15 22:56:17 2006 +0200
@@ -7,8 +7,6 @@
 
 signature BASIC_THEORY =
 sig
-  type theory
-  type theory_ref
   val sign_of: theory -> theory    (*obsolete*)
   val rep_theory: theory ->
    {axioms: term NameSpace.table,
@@ -63,9 +61,6 @@
 
 (* context operations *)
 
-type theory = Context.theory;
-type theory_ref = Context.theory_ref;
-
 val eq_thy = Context.eq_thy;
 val subthy = Context.subthy;