# HG changeset patch
# User wenzelm
# Date 1158353777 -7200
# Node ID c643984eb94b3f4d5e2da496cbadd225be7f777b
# Parent  8ef25fe585a88fb2a1b39ce2dc54891a49683698
removed type aliases for theory/theory_ref;

diff -r 8ef25fe585a8 -r c643984eb94b src/Pure/theory.ML
--- 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;