# HG changeset patch
# User wenzelm
# Date 891682860 -7200
# Node ID 9b6072bd71e4eec8a3050a509df2640b8094d14a
# Parent  52fa5258db2ea4542f783aa28495f6c6f2e20922
added local_theory (for Isar);
added setup;

diff -r 52fa5258db2e -r 9b6072bd71e4 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Sat Apr 04 11:40:18 1998 +0200
+++ b/src/Pure/theory.ML	Sat Apr 04 11:41:00 1998 +0200
@@ -10,6 +10,7 @@
 signature BASIC_THEORY =
 sig
   type theory
+  type local_theory
   exception THEORY of string * theory list
   val rep_theory: theory ->
     {sign: Sign.sg,
@@ -77,6 +78,7 @@
     (object * object -> object) * (Sign.sg -> object -> unit))) list -> theory -> theory
   val get_data: theory -> string -> object
   val put_data: string * object -> theory -> theory
+  val setup: (theory -> theory) list -> theory -> theory
   val prep_ext: theory -> theory
   val prep_ext_merge: theory list -> theory
   val pre_pure: theory
@@ -97,6 +99,9 @@
     parents: theory list,
     ancestors: theory list};
 
+(*forward definition for Isar proof contexts*)
+type local_theory = theory * object Symtab.table;
+
 fun make_thy sign axms oras parents ancestors =
   Theory {sign = sign, axioms = axms, oracles = oras,
     parents = parents, ancestors = ancestors};
@@ -380,6 +385,10 @@
 val get_data = Sign.get_data o sign_of;
 val put_data = ext_sg Sign.put_data;
 
+(*generic setup*)
+fun setup [] thy = thy
+  | setup (f :: fs) thy = setup fs (f thy);
+
 
 
 (** merge theories **)		(*exception ERROR*)