removed local_theory;
authorwenzelm
Mon Nov 09 15:40:05 1998 +0100 (1998-11-09)
changeset 5837ce9a8b05d652
parent 5836 90f7d9f1a0cc
child 5838 a4122945d638
removed local_theory;
src/Pure/theory.ML
     1.1 --- a/src/Pure/theory.ML	Mon Nov 09 15:39:31 1998 +0100
     1.2 +++ b/src/Pure/theory.ML	Mon Nov 09 15:40:05 1998 +0100
     1.3 @@ -9,7 +9,6 @@
     1.4  signature BASIC_THEORY =
     1.5  sig
     1.6    type theory
     1.7 -  type local_theory
     1.8    exception THEORY of string * theory list
     1.9    val rep_theory: theory ->
    1.10      {sign: Sign.sg,
    1.11 @@ -110,9 +109,6 @@
    1.12      parents: theory list,
    1.13      ancestors: theory list};
    1.14  
    1.15 -(*forward definition for Isar proof contexts*)
    1.16 -type local_theory = theory * Object.T Symtab.table;
    1.17 -
    1.18  fun make_theory sign axms oras parents ancestors =
    1.19    Theory {sign = sign, axioms = axms, oracles = oras,
    1.20      parents = parents, ancestors = ancestors};