# HG changeset patch
# User wenzelm
# Date 910622405 -3600
# Node ID ce9a8b05d652904a4ae2ed6ff880184ed31bfb2f
# Parent  90f7d9f1a0ccd1da797ad8a50b5f3530d0f7317a
removed local_theory;

diff -r 90f7d9f1a0cc -r ce9a8b05d652 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Mon Nov 09 15:39:31 1998 +0100
+++ b/src/Pure/theory.ML	Mon Nov 09 15:40:05 1998 +0100
@@ -9,7 +9,6 @@
 signature BASIC_THEORY =
 sig
   type theory
-  type local_theory
   exception THEORY of string * theory list
   val rep_theory: theory ->
     {sign: Sign.sg,
@@ -110,9 +109,6 @@
     parents: theory list,
     ancestors: theory list};
 
-(*forward definition for Isar proof contexts*)
-type local_theory = theory * Object.T Symtab.table;
-
 fun make_theory sign axms oras parents ancestors =
   Theory {sign = sign, axioms = axms, oracles = oras,
     parents = parents, ancestors = ancestors};