--- 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};