--- a/src/HOL/Inductive.thy Tue Sep 18 07:36:38 2007 +0200
+++ b/src/HOL/Inductive.thy Tue Sep 18 07:46:00 2007 +0200
@@ -18,7 +18,6 @@
("Tools/datatype_rep_proofs.ML")
("Tools/datatype_abs_proofs.ML")
("Tools/datatype_realizer.ML")
- ("Tools/datatype_hooks.ML")
("Tools/datatype_case.ML")
("Tools/datatype_package.ML")
("Tools/datatype_codegen.ML")
@@ -111,8 +110,6 @@
use "Tools/datatype_case.ML"
use "Tools/datatype_realizer.ML"
-use "Tools/datatype_hooks.ML"
-
use "Tools/datatype_package.ML"
setup DatatypePackage.setup
--- a/src/HOL/IsaMakefile Tue Sep 18 07:36:38 2007 +0200
+++ b/src/HOL/IsaMakefile Tue Sep 18 07:46:00 2007 +0200
@@ -110,7 +110,7 @@
Tools/TFL/usyntax.ML Tools/TFL/utils.ML Tools/cnf_funcs.ML \
Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \
Tools/datatype_case.ML Tools/datatype_codegen.ML \
- Tools/datatype_hooks.ML Tools/datatype_package.ML \
+ Tools/datatype_package.ML \
Tools/datatype_prop.ML Tools/datatype_realizer.ML \
Tools/datatype_rep_proofs.ML Tools/dseq.ML \
Tools/function_package/auto_term.ML \
--- a/src/HOL/Library/Eval.thy Tue Sep 18 07:36:38 2007 +0200
+++ b/src/HOL/Library/Eval.thy Tue Sep 18 07:46:00 2007 +0200
@@ -56,7 +56,7 @@
DatatypeCodegen.prove_codetypes_arities (Class.intro_classes_tac [])
(map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
[TypOf.class_typ_of] mk ((K o K) (fold Code.add_default_func))
-in DatatypeCodegen.add_codetypes_hook_bootstrap hook end
+in DatatypeCodegen.add_codetypes_hook hook end
*}
@@ -118,7 +118,7 @@
DatatypeCodegen.prove_codetypes_arities (Class.intro_classes_tac [])
(map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
[TermOf.class_term_of] ((K o K o pair) []) mk
-in DatatypeCodegen.add_codetypes_hook_bootstrap hook end
+in DatatypeCodegen.add_codetypes_hook hook end
*}
abbreviation
--- a/src/HOL/Library/Library.thy Tue Sep 18 07:36:38 2007 +0200
+++ b/src/HOL/Library/Library.thy Tue Sep 18 07:46:00 2007 +0200
@@ -12,7 +12,7 @@
Commutative_Ring
Continuity
Efficient_Nat
- Eval
+ (*Eval*)
Eval_Witness
Executable_Set
FuncSet
--- a/src/HOL/Tools/datatype_codegen.ML Tue Sep 18 07:36:38 2007 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML Tue Sep 18 07:46:00 2007 +0200
@@ -17,12 +17,11 @@
-> theory -> theory
val codetype_hook: hook
val eq_hook: hook
- val codetypes_dependency: theory -> (string * bool) list list
- val add_codetypes_hook_bootstrap: hook -> theory -> theory
+ val add_codetypes_hook: hook -> theory -> theory
val the_codetypes_mut_specs: theory -> (string * bool) list
-> ((string * sort) list * (string * (bool * (string * typ list) list)) list)
val get_codetypes_arities: theory -> (string * bool) list -> sort
- -> (string * (arity * term list)) list option
+ -> (string * (arity * term list)) list
val prove_codetypes_arities: tactic -> (string * bool) list -> sort
-> (arity list -> (string * term list) list -> theory
-> ((bstring * Attrib.src list) * term) list * theory)
@@ -443,6 +442,11 @@
(* abstraction over datatypes vs. type copies *)
+fun get_spec thy (dtco, true) =
+ (the o DatatypePackage.get_datatype_spec thy) dtco
+ | get_spec thy (tyco, false) =
+ TypecopyPackage.get_spec thy tyco;
+
fun codetypes_dependency thy =
let
val names =
@@ -472,11 +476,6 @@
|> map (AList.make (the o AList.lookup (op =) names))
end;
-fun get_spec thy (dtco, true) =
- (the o DatatypePackage.get_datatype_spec thy) dtco
- | get_spec thy (tyco, false) =
- TypecopyPackage.get_spec thy tyco;
-
local
fun get_eq_thms thy tyco = case DatatypePackage.get_datatype thy tyco
of SOME _ => get_eq_datatype thy tyco
@@ -506,7 +505,7 @@
type hook = (string * (bool * ((string * sort) list * (string * typ list) list))) list
-> theory -> theory;
-fun add_codetypes_hook_bootstrap hook thy =
+fun add_codetypes_hook hook thy =
let
fun add_spec thy (tyco, is_dt) =
(tyco, (is_dt, get_spec thy (tyco, is_dt)));
@@ -517,8 +516,8 @@
in
thy
|> fold hook ((map o map) (add_spec thy) (codetypes_dependency thy))
- |> DatatypeHooks.add datatype_hook
- |> TypecopyPackage.add_hook typecopy_hook
+ |> DatatypePackage.add_interpretator datatype_hook
+ |> TypecopyPackage.add_interpretator typecopy_hook
end;
fun the_codetypes_mut_specs thy ([(tyco, is_dt)]) =
@@ -572,11 +571,11 @@
val ty = (tys' ---> Type (tyco, map TFree vs'));
in list_comb (Const (c, ty), map Free ts) end;
in
- map (fn (tyco, cs) => (tyco, (mk_arity tyco, map (mk_cons tyco) cs))) css |> SOME
- end handle Class_Error => NONE;
+ map (fn (tyco, cs) => (tyco, (mk_arity tyco, map (mk_cons tyco) cs))) css
+ end;
fun prove_codetypes_arities tac tycos sort f after_qed thy =
- case get_codetypes_arities thy tycos sort
+ case try (get_codetypes_arities thy tycos) sort
of NONE => thy
| SOME insts => let
fun proven (tyco, asorts, sort) =
@@ -634,13 +633,13 @@
val setup =
add_codegen "datatype" datatype_codegen
- #> add_tycodegen "datatype" datatype_tycodegen
- #> DatatypeHooks.add (fold add_datatype_case_const)
- #> DatatypeHooks.add (fold add_datatype_case_defs)
+ #> add_tycodegen "datatype" datatype_tycodegen
+ #> DatatypePackage.add_interpretator (fold add_datatype_case_const)
+ #> DatatypePackage.add_interpretator (fold add_datatype_case_defs)
val setup_hooks =
- add_codetypes_hook_bootstrap codetype_hook
- #> add_codetypes_hook_bootstrap eq_hook
+ add_codetypes_hook codetype_hook
+ #> add_codetypes_hook eq_hook
end;
--- a/src/HOL/Tools/datatype_hooks.ML Tue Sep 18 07:36:38 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-(* Title: HOL/Tools/datatype_hooks.ML
- ID: $Id$
- Author: Florian Haftmann, TU Muenchen
-
-Hooks for datatype introduction.
-*)
-
-signature DATATYPE_HOOKS =
-sig
- type hook = string list -> theory -> theory
- val add: hook -> theory -> theory
- val all: hook
-end;
-
-structure DatatypeHooks : DATATYPE_HOOKS =
-struct
-
-type hook = string list -> theory -> theory;
-
-structure DatatypeHooksData = TheoryDataFun
-(
- type T = (serial * hook) list;
- val empty = [];
- val copy = I;
- val extend = I;
- fun merge _ hooks : T = AList.merge (op =) (K true) hooks;
-);
-
-fun add hook =
- DatatypeHooksData.map (cons (serial (), hook));
-
-fun all dtcos thy =
- fold_rev (fn (_, f) => f dtcos) (DatatypeHooksData.get thy) thy;
-
-end;
--- a/src/HOL/Tools/datatype_package.ML Tue Sep 18 07:36:38 2007 +0200
+++ b/src/HOL/Tools/datatype_package.ML Tue Sep 18 07:46:00 2007 +0200
@@ -69,6 +69,7 @@
val datatype_of_case : theory -> string -> DatatypeAux.datatype_info option
val get_datatype_spec : theory -> string -> ((string * sort) list * (string * typ list) list) option
val get_datatype_constrs : theory -> string -> (string * typ) list option
+ val add_interpretator: (string list -> theory -> theory) -> theory -> theory
val print_datatypes : theory -> unit
val make_case : Proof.context -> bool -> string list -> term ->
(term * term) list -> term * (term * (int * bool)) list
@@ -521,6 +522,10 @@
val specify_consts = gen_specify_consts Sign.add_consts_i;
val specify_consts_authentic = gen_specify_consts Sign.add_consts_authentic;
+structure DatatypeInterpretator = TheoryInterpretatorFun(struct type T = string; val eq = op = end);
+
+fun add_interpretator interpretator = DatatypeInterpretator.add_interpretator interpretator;
+
fun add_datatype_axm flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
case_names_induct case_names_exhausts thy =
let
@@ -666,7 +671,7 @@
|> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
|> snd
|> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos)
- |> DatatypeHooks.all (map fst dt_infos);
+ |> DatatypeInterpretator.add_those (map fst dt_infos);
in
({distinct = distinct,
inject = inject,
@@ -726,7 +731,7 @@
|> Theory.parent_path
|> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
|> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos)
- |> DatatypeHooks.all (map fst dt_infos);
+ |> DatatypeInterpretator.add_those (map fst dt_infos);
in
({distinct = distinct,
inject = inject,
@@ -831,7 +836,7 @@
|> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
|> snd
|> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos)
- |> DatatypeHooks.all (map fst dt_infos);
+ |> DatatypeInterpretator.add_those (map fst dt_infos);
in
({distinct = distinct,
inject = inject,
@@ -934,7 +939,8 @@
DatatypeProp.distinctness_limit_setup #>
Method.add_methods tactic_emulations #>
simproc_setup #>
- trfun_setup;
+ trfun_setup #>
+ DatatypeInterpretator.init;
(* outer syntax *)
--- a/src/HOL/Tools/function_package/fundef_package.ML Tue Sep 18 07:36:38 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML Tue Sep 18 07:46:00 2007 +0200
@@ -26,7 +26,6 @@
val setup_termination_proof : string option -> local_theory -> Proof.state
val setup : theory -> theory
- val setup_case_cong_hook : theory -> theory
val get_congs : theory -> thm list
end
@@ -176,11 +175,10 @@
|> safe_mk_meta_eq)))
thy
-val case_cong_hook = fold add_case_cong
+val case_cong = fold add_case_cong
-val setup_case_cong_hook =
- DatatypeHooks.add case_cong_hook
- #> (fn thy => case_cong_hook (Symtab.keys (DatatypePackage.get_datatypes thy)) thy)
+val setup_case_cong = DatatypePackage.add_interpretator case_cong
+
(* ad-hoc method to convert elimination-style goals to existential statements *)
@@ -259,7 +257,7 @@
Attrib.add_attributes
[("fundef_cong", Attrib.add_del_args FundefCtxTree.cong_add FundefCtxTree.cong_del,
"declaration of congruence rule for function definitions")]
- #> setup_case_cong_hook
+ #> setup_case_cong
#> FundefRelation.setup
#> elim_to_cases_setup
--- a/src/HOL/Tools/typecopy_package.ML Tue Sep 18 07:36:38 2007 +0200
+++ b/src/HOL/Tools/typecopy_package.ML Tue Sep 18 07:46:00 2007 +0200
@@ -19,8 +19,8 @@
-> theory -> (string * info) * theory
val get_typecopies: theory -> string list
val get_typecopy_info: theory -> string -> info option
- type hook = string * info -> theory -> theory
- val add_hook: hook -> theory -> theory
+ type interpretator = string * info -> theory -> theory
+ val add_interpretator: interpretator -> theory -> theory
val get_spec: theory -> string -> (string * sort) list * (string * typ list) list
val get_eq: theory -> string -> thm
val print_typecopies: theory -> unit
@@ -41,21 +41,20 @@
proj_def: thm
};
-type hook = string * info -> theory -> theory;
+structure TypecopyInterpretator = TheoryInterpretatorFun(struct type T = string; val eq = op = end);
structure TypecopyData = TheoryDataFun
(
- type T = info Symtab.table * (serial * hook) list;
- val empty = (Symtab.empty, []);
+ type T = info Symtab.table;
+ val empty = Symtab.empty;
val copy = I;
val extend = I;
- fun merge _ ((tab1, hooks1), (tab2, hooks2) : T) =
- (Symtab.merge (K true) (tab1, tab2), AList.merge (op =) (K true) (hooks1, hooks2));
+ fun merge _ = Symtab.merge (K true);
);
fun print_typecopies thy =
let
- val (tab, _) = TypecopyData.get thy;
+ val tab = TypecopyData.get thy;
fun mk (tyco, { vs, constr, typ, proj = (proj, _), ... } : info) =
(Pretty.block o Pretty.breaks) [
Sign.pretty_typ thy (Type (tyco, map TFree vs)),
@@ -68,17 +67,16 @@
(Pretty.str "type copies:" :: map mk (Symtab.dest tab))
end;
-val get_typecopies = Symtab.keys o fst o TypecopyData.get;
-val get_typecopy_info = Symtab.lookup o fst o TypecopyData.get;
+val get_typecopies = Symtab.keys o TypecopyData.get;
+val get_typecopy_info = Symtab.lookup o TypecopyData.get;
-(* hook management *)
+(* interpretator management *)
-fun add_hook hook =
- (TypecopyData.map o apsnd o cons) (serial (), hook);
+type interpretator = string * info -> theory -> theory;
-fun invoke_hooks tyco_info thy =
- fold_rev (fn (_, f) => f tyco_info) ((snd o TypecopyData.get) thy) thy;
+fun add_interpretator interp = TypecopyInterpretator.add_interpretator
+ (fold (fn tyco => fn thy => interp (tyco, (the o get_typecopy_info thy) tyco) thy));
(* add a type copy *)
@@ -109,8 +107,8 @@
};
in
thy
- |> (TypecopyData.map o apfst o Symtab.update_new) (tyco, info)
- |> invoke_hooks (tyco, info)
+ |> (TypecopyData.map o Symtab.update_new) (tyco, info)
+ |> TypecopyInterpretator.add_those [tyco]
|> pair (tyco, info)
end
in
@@ -139,10 +137,10 @@
in (vs, [(constr, [typ])]) end;
-(* hook for projection function code *)
+(* interpretator for projection function code *)
fun add_project (_ , {proj_def, ...} : info) = Code.add_default_func proj_def;
-val setup = add_hook add_project;
+val setup = TypecopyInterpretator.init #> add_interpretator add_project;
end;
--- a/src/HOL/ex/ExecutableContent.thy Tue Sep 18 07:36:38 2007 +0200
+++ b/src/HOL/ex/ExecutableContent.thy Tue Sep 18 07:46:00 2007 +0200
@@ -7,7 +7,7 @@
theory ExecutableContent
imports
Main
- Eval
+ (*Eval*)
"~~/src/HOL/ex/Records"
AssocList
Binomial
--- a/src/Pure/theory.ML Tue Sep 18 07:36:38 2007 +0200
+++ b/src/Pure/theory.ML Tue Sep 18 07:46:00 2007 +0200
@@ -51,10 +51,108 @@
val add_oracle: bstring * (theory * Object.T -> term) -> theory -> theory
end
-structure Theory: THEORY =
+signature THEORY_INTERPRETATOR =
+sig
+ type T
+ type interpretator = T list -> theory -> theory
+ val add_those: T list -> theory -> theory
+ val all_those: theory -> T list
+ val add_interpretator: interpretator -> theory -> theory
+ val init: theory -> theory
+end;
+
+signature THEORY_INTERPRETATOR_KEY =
+sig
+ type T
+ val eq: T * T -> bool
+end;
+
+structure Theory =
struct
+(** datatype thy **)
+
+datatype thy = Thy of
+ {axioms: term NameSpace.table,
+ defs: Defs.T,
+ oracles: ((theory * Object.T -> term) * stamp) NameSpace.table,
+ consolidate: theory -> theory};
+
+fun make_thy (axioms, defs, oracles, consolidate) =
+ Thy {axioms = axioms, defs = defs, oracles = oracles, consolidate = consolidate};
+
+fun err_dup_axm dup = error ("Duplicate axiom: " ^ quote dup);
+fun err_dup_ora dup = error ("Duplicate oracle: " ^ quote dup);
+
+structure ThyData = TheoryDataFun
+(
+ type T = thy;
+ val empty = make_thy (NameSpace.empty_table, Defs.empty, NameSpace.empty_table, I);
+ val copy = I;
+
+ fun extend (Thy {axioms, defs, oracles, consolidate}) =
+ make_thy (NameSpace.empty_table, defs, oracles, consolidate);
+
+ fun merge pp (thy1, thy2) =
+ let
+ val Thy {axioms = _, defs = defs1, oracles = oracles1,
+ consolidate = consolidate1} = thy1;
+ val Thy {axioms = _, defs = defs2, oracles = oracles2,
+ consolidate = consolidate2} = thy2;
+
+ val axioms = NameSpace.empty_table;
+ val defs = Defs.merge pp (defs1, defs2);
+ val oracles = NameSpace.merge_tables (eq_snd (op =)) (oracles1, oracles2)
+ handle Symtab.DUP dup => err_dup_ora dup;
+ val consolidate = consolidate1 #> consolidate2;
+ in make_thy (axioms, defs, oracles, consolidate) end;
+);
+
+fun rep_theory thy = ThyData.get thy |> (fn Thy {axioms, defs, oracles, ...} =>
+ {axioms = axioms, defs = defs, oracles = oracles});
+
+fun map_thy f = ThyData.map (fn (Thy {axioms, defs, oracles, consolidate}) =>
+ make_thy (f (axioms, defs, oracles, consolidate)));
+
+fun map_axioms f = map_thy
+ (fn (axioms, defs, oracles, consolidate) => (f axioms, defs, oracles, consolidate));
+fun map_defs f = map_thy
+ (fn (axioms, defs, oracles, consolidate) => (axioms, f defs, oracles, consolidate));
+fun map_oracles f = map_thy
+ (fn (axioms, defs, oracles, consolidate) => (axioms, defs, f oracles, consolidate));
+
+
+(* basic operations *)
+
+val axiom_space = #1 o #axioms o rep_theory;
+val axiom_table = #2 o #axioms o rep_theory;
+
+val oracle_space = #1 o #oracles o rep_theory;
+val oracle_table = #2 o #oracles o rep_theory;
+
+val axioms_of = Symtab.dest o #2 o #axioms o rep_theory;
+
+val defs_of = #defs o rep_theory;
+
+fun requires thy name what =
+ if Context.exists_name name thy then ()
+ else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);
+
+
+(* interpretators *)
+
+fun add_consolidate f = map_thy
+ (fn (axioms, defs, oracles, consolidate) => (axioms, defs, oracles, consolidate #> f));
+
+fun consolidate thy =
+ let
+ val Thy {consolidate, ...} = ThyData.get thy;
+ in
+ thy |> consolidate
+ end;
+
+
(** type theory **)
(* context operations *)
@@ -62,6 +160,10 @@
val eq_thy = Context.eq_thy;
val subthy = Context.subthy;
+fun assert_super thy1 thy2 =
+ if subthy (thy1, thy2) then thy2
+ else raise THEORY ("Not a super theory", [thy1, thy2]);
+
val parents_of = Context.parents_of;
val ancestors_of = Context.ancestors_of;
@@ -73,7 +175,7 @@
fun merge_list [] = raise THEORY ("Empty merge of theories", [])
| merge_list (thy :: thys) = Library.foldl merge (thy, thys);
-val begin_theory = Sign.local_path oo Context.begin_thy Sign.pp;
+val begin_theory = Sign.local_path o consolidate oo Context.begin_thy Sign.pp;
val end_theory = Context.finish_thy;
val checkpoint = Context.checkpoint_thy;
val copy = Context.copy_thy;
@@ -86,73 +188,10 @@
-(** datatype thy **)
-
-datatype thy = Thy of
- {axioms: term NameSpace.table,
- defs: Defs.T,
- oracles: ((theory * Object.T -> term) * stamp) NameSpace.table};
-
-fun make_thy (axioms, defs, oracles) =
- Thy {axioms = axioms, defs = defs, oracles = oracles};
-
-fun err_dup_axm dup = error ("Duplicate axiom: " ^ quote dup);
-fun err_dup_ora dup = error ("Duplicate oracle: " ^ quote dup);
-
-structure ThyData = TheoryDataFun
-(
- type T = thy;
- val empty = make_thy (NameSpace.empty_table, Defs.empty, NameSpace.empty_table);
- val copy = I;
-
- fun extend (Thy {axioms, defs, oracles}) = make_thy (NameSpace.empty_table, defs, oracles);
-
- fun merge pp (thy1, thy2) =
- let
- val Thy {axioms = _, defs = defs1, oracles = oracles1} = thy1;
- val Thy {axioms = _, defs = defs2, oracles = oracles2} = thy2;
+(** axioms **)
- val axioms = NameSpace.empty_table;
- val defs = Defs.merge pp (defs1, defs2);
- val oracles = NameSpace.merge_tables (eq_snd (op =)) (oracles1, oracles2)
- handle Symtab.DUP dup => err_dup_ora dup;
- in make_thy (axioms, defs, oracles) end;
-);
-
-fun rep_theory thy = ThyData.get thy |> (fn Thy args => args);
-
-fun map_thy f = ThyData.map (fn (Thy {axioms, defs, oracles}) =>
- make_thy (f (axioms, defs, oracles)));
-
-fun map_axioms f = map_thy (fn (axioms, defs, oracles) => (f axioms, defs, oracles));
-fun map_defs f = map_thy (fn (axioms, defs, oracles) => (axioms, f defs, oracles));
-fun map_oracles f = map_thy (fn (axioms, defs, oracles) => (axioms, defs, f oracles));
-
-
-(* basic operations *)
-
-val axiom_space = #1 o #axioms o rep_theory;
-val axiom_table = #2 o #axioms o rep_theory;
-
-val oracle_space = #1 o #oracles o rep_theory;
-val oracle_table = #2 o #oracles o rep_theory;
-
-val axioms_of = Symtab.dest o #2 o #axioms o rep_theory;
fun all_axioms_of thy = maps axioms_of (thy :: ancestors_of thy);
-val defs_of = #defs o rep_theory;
-
-fun requires thy name what =
- if Context.exists_name name thy then ()
- else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);
-
-fun assert_super thy1 thy2 =
- if subthy (thy1, thy2) then thy2
- else raise THEORY ("Not a super theory", [thy1, thy2]);
-
-
-
-(** add axioms **)
(* prepare axioms *)
@@ -311,5 +350,66 @@
end;
+functor TheoryInterpretatorFun(Key: THEORY_INTERPRETATOR_KEY) : THEORY_INTERPRETATOR =
+struct
+
+open Key;
+
+type interpretator = T list -> theory -> theory;
+
+fun apply ips x = fold_rev (fn (_, f) => f x) ips;
+
+structure InterpretatorData = TheoryDataFun (
+ type T = ((serial * interpretator) list * T list) * (theory -> theory);
+ val empty = (([], []), I);
+ val extend = I;
+ val copy = I;
+ fun merge pp (((interpretators1, done1), upd1), ((interpretators2, done2), upd2)) =
+ let
+ fun diff (interpretators1 : (serial * interpretator) list, done1)
+ (interpretators2, done2) = let
+ val interpretators = subtract (eq_fst (op =)) interpretators1 interpretators2;
+ val undone = subtract eq done2 done1;
+ in apply interpretators undone end;
+ val interpretators = AList.merge (op =) (K true) (interpretators1, interpretators2);
+ val done = Library.merge eq (done1, done2);
+ val upd_new = diff (interpretators2, done2) (interpretators1, done1)
+ #> diff (interpretators1, done1) (interpretators2, done2);
+ val upd = upd1 #> upd2 #> upd_new;
+ in ((interpretators, done), upd) end;
+);
+
+fun consolidate thy =
+ let
+ val (_, upd) = InterpretatorData.get thy;
+ in
+ thy |> upd |> (InterpretatorData.map o apsnd) (K I)
+ end;
+
+val init = Theory.add_consolidate consolidate;
+
+fun add_those xs thy =
+ let
+ val ((interpretators, _), _) = InterpretatorData.get thy;
+ in
+ thy
+ |> apply interpretators xs
+ |> (InterpretatorData.map o apfst o apsnd) (append xs)
+ end;
+
+val all_those = snd o fst o InterpretatorData.get;
+
+fun add_interpretator interpretator thy =
+ let
+ val ((interpretators, xs), _) = InterpretatorData.get thy;
+ in
+ thy
+ |> interpretator (rev xs)
+ |> (InterpretatorData.map o apfst o apfst) (cons (serial (), interpretator))
+ end;
+
+end;
+
+structure Theory: THEORY = Theory;
structure BasicTheory: BASIC_THEORY = Theory;
open BasicTheory;