--- 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*)