--- a/doc-src/IsarImplementation/Thy/integration.thy Fri Mar 28 19:43:54 2008 +0100
+++ b/doc-src/IsarImplementation/Thy/integration.thy Fri Mar 28 20:02:04 2008 +0100
@@ -241,7 +241,7 @@
text %mlref {*
\begin{mldecls}
@{index_ML the_context: "unit -> theory"} \\
- @{index_ML "Context.>> ": "(theory -> theory) -> unit"} \\
+ @{index_ML "Context.>> ": "(Context.generic -> Context.generic) -> unit"} \\
\end{mldecls}
\begin{description}
@@ -255,13 +255,8 @@
information immediately, or produce an explicit @{ML_type
theory_ref} (cf.\ \secref{sec:context-theory}).
- \item @{ML "Context.>>"}~@{text f} applies theory transformation
- @{text f} to the current theory of the {\ML} toplevel. In order to
- work as expected, the theory should be still under construction, and
- the Isar language element that invoked the {\ML} compiler in the
- first place should be ready to accept the changed theory value
- (e.g.\ \isakeyword{ML-setup}, but not plain \isakeyword{ML}).
- Otherwise the theory becomes stale!
+ \item @{ML "Context.>>"}~@{text f} applies context transformation
+ @{text f} to the implicit context of the {\ML} toplevel.
\end{description}
--- a/src/Pure/Isar/attrib.ML Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/Isar/attrib.ML Fri Mar 28 20:02:04 2008 +0100
@@ -276,7 +276,7 @@
(* theory setup *)
-val _ = Context.>>
+val _ = Context.>> (Context.map_theory
(add_attributes
[("attribute", internal_att, "internal attribute"),
("tagged", tagged, "tagged theorem"),
@@ -301,7 +301,7 @@
("rule_format", rule_format, "result put into standard rule format"),
("rotated", rotated, "rotated theorem premises"),
("defn", add_del_args LocalDefs.defn_add LocalDefs.defn_del,
- "declaration of definitional transformations")]);
+ "declaration of definitional transformations")]));
@@ -379,12 +379,12 @@
(* theory setup *)
-val _ = Context.>>
+val _ = Context.>> (Context.map_theory
(register_config Unify.trace_bound_value #>
register_config Unify.search_bound_value #>
register_config Unify.trace_simp_value #>
register_config Unify.trace_types_value #>
- register_config MetaSimplifier.simp_depth_limit_value);
+ register_config MetaSimplifier.simp_depth_limit_value));
end;
--- a/src/Pure/Isar/calculation.ML Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/Isar/calculation.ML Fri Mar 28 20:02:04 2008 +0100
@@ -92,14 +92,14 @@
val trans_att = Attrib.add_del_args trans_add trans_del;
val sym_att = Attrib.add_del_args sym_add sym_del;
-val _ = Context.>>
+val _ = Context.>> (Context.map_theory
(Attrib.add_attributes
[("trans", trans_att, "declaration of transitivity rule"),
("sym", sym_att, "declaration of symmetry rule"),
("symmetric", Attrib.no_args symmetric, "resolution with symmetry rule")] #>
PureThy.add_thms
[(("", transitive_thm), [trans_add]),
- (("", symmetric_thm), [sym_add])] #> snd);
+ (("", symmetric_thm), [sym_add])] #> snd));
--- a/src/Pure/Isar/class.ML Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/Isar/class.ML Fri Mar 28 20:02:04 2008 +0100
@@ -140,7 +140,7 @@
fun mk_class_data ((consts, base_sort, inst, morphism, assm_intro, of_class, axiom),
(defs, operations)) =
ClassData { consts = consts, base_sort = base_sort, inst = inst,
- morphism = morphism, assm_intro = assm_intro, of_class = of_class, axiom = axiom,
+ morphism = morphism, assm_intro = assm_intro, of_class = of_class, axiom = axiom,
defs = defs, operations = operations };
fun map_class_data f (ClassData { consts, base_sort, inst, morphism,
assm_intro, of_class, axiom, defs, operations }) =
@@ -304,7 +304,7 @@
#> map_types subst_typ;
fun subst_thm defs = Drule.standard' #> instantiate_class #> lift_axiom
#> MetaSimplifier.rewrite_rule defs;
- fun morphism thy defs =
+ fun morphism thy defs =
Morphism.typ_morphism subst_typ
$> Morphism.term_morphism (subst_term thy defs)
$> Morphism.thm_morphism (subst_thm defs);
@@ -395,11 +395,13 @@
HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
default_intro_classes_tac facts;
-val _ = Context.>> (Method.add_methods
- [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
- "back-chain introduction rules of classes"),
- ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac),
- "apply some intro/elim rule")]);
+val _ = Context.>> (Context.map_theory
+ (Method.add_methods
+ [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
+ "back-chain introduction rules of classes"),
+ ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac),
+ "apply some intro/elim rule")]));
+
(** classes and class target **)
--- a/src/Pure/Isar/code.ML Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/Isar/code.ML Fri Mar 28 20:02:04 2008 +0100
@@ -107,8 +107,9 @@
val code_attr = Attrib.syntax (Scan.peek (fn context =>
List.foldr op || Scan.fail (map snd (CodeAttr.get (Context.theory_of context)))));
in
- Context.>> (Attrib.add_attributes
- [("code", code_attr, "declare theorems for code generation")])
+ Context.>> (Context.map_theory
+ (Attrib.add_attributes
+ [("code", code_attr, "declare theorems for code generation")]))
end;
@@ -387,7 +388,7 @@
in (exec, ref data) end;
);
-val _ = Context.>> CodeData.init;
+val _ = Context.>> (Context.map_theory CodeData.init);
fun thy_data f thy = f ((snd o CodeData.get) thy);
@@ -864,7 +865,7 @@
(remove Thm.eq_thm_prop (CodeUnit.error_thm CodeUnit.mk_rew thm)) thy;
(*fully applied in order to get right context for mk_rew!*)
-val _ = Context.>>
+val _ = Context.>> (Context.map_theory
(let
fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
fun add_simple_attribute (name, f) =
@@ -877,7 +878,7 @@
#> add_del_attribute ("func", (add_func, del_func))
#> add_del_attribute ("inline", (add_inline, del_inline))
#> add_del_attribute ("post", (add_post, del_post))
- end);
+ end));
(** post- and preprocessing **)
--- a/src/Pure/Isar/context_rules.ML Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/Isar/context_rules.ML Fri Mar 28 20:02:04 2008 +0100
@@ -198,8 +198,8 @@
val elim_query = rule_add elim_queryK I;
val dest_query = rule_add elim_queryK Tactic.make_elim;
-val _ = Context.>>
- (snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [intro_query NONE])]);
+val _ = Context.>> (Context.map_theory
+ (snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [intro_query NONE])]));
(* concrete syntax *)
@@ -215,6 +215,6 @@
("rule", Attrib.syntax (Scan.lift Args.del >> K rule_del),
"remove declaration of intro/elim/dest rule")];
-val _ = Context.>> (Attrib.add_attributes rule_atts);
+val _ = Context.>> (Context.map_theory (Attrib.add_attributes rule_atts));
end;
--- a/src/Pure/Isar/isar_cmd.ML Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Fri Mar 28 20:02:04 2008 +0100
@@ -204,7 +204,8 @@
\ val oracle: theory -> T -> term = " ^ oracle ^ ";\n\
\ val name = " ^ quote name ^ ";\n\
\ exception Arg of T;\n\
- \ val _ = Context.>> (Theory.add_oracle (name, fn (thy, Arg x) => oracle thy x));\n\
+ \ val _ = Context.>> (Context.map_theory\n\
+ \ (Theory.add_oracle (name, fn (thy, Arg x) => oracle thy x)));\n\
\ val thy = ML_Context.the_global_context ();\n\
\ val invoke_" ^ name ^ " = Thm.invoke_oracle_i thy (Sign.full_name thy name);\n\
\in\n\
--- a/src/Pure/Isar/locale.ML Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/Isar/locale.ML Fri Mar 28 20:02:04 2008 +0100
@@ -2000,11 +2000,11 @@
end;
-val _ = Context.>>
+val _ = Context.>> (Context.map_theory
(add_locale_i (SOME "") "var" empty [Fixes [(Name.internal "x", NONE, NoSyn)]] #>
snd #> ProofContext.theory_of #>
add_locale_i (SOME "") "struct" empty [Fixes [(Name.internal "S", NONE, Structure)]] #>
- snd #> ProofContext.theory_of);
+ snd #> ProofContext.theory_of));
@@ -2041,13 +2041,14 @@
Method.intros_tac (wits @ intros) facts st
end;
-val _ = Context.>> (Method.add_methods
- [("intro_locales",
- Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt)),
- "back-chain introduction rules of locales without unfolding predicates"),
- ("unfold_locales",
- Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac true ctxt)),
- "back-chain all introduction rules of locales")]);
+val _ = Context.>> (Context.map_theory
+ (Method.add_methods
+ [("intro_locales",
+ Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt)),
+ "back-chain introduction rules of locales without unfolding predicates"),
+ ("unfold_locales",
+ Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac true ctxt)),
+ "back-chain all introduction rules of locales")]));
end;
--- a/src/Pure/Isar/method.ML Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/Isar/method.ML Fri Mar 28 20:02:04 2008 +0100
@@ -554,31 +554,33 @@
(* theory setup *)
-val _ = Context.>> (add_methods
- [("fail", no_args fail, "force failure"),
- ("succeed", no_args succeed, "succeed"),
- ("-", no_args insert_facts, "do nothing (insert current facts only)"),
- ("insert", thms_args insert, "insert theorems, ignoring facts (improper)"),
- ("intro", thms_args intro, "repeatedly apply introduction rules"),
- ("elim", thms_args elim, "repeatedly apply elimination rules"),
- ("unfold", thms_ctxt_args unfold_meth, "unfold definitions"),
- ("fold", thms_ctxt_args fold_meth, "fold definitions"),
- ("atomize", (atomize o fst) oo syntax (Args.mode "full"),
- "present local premises as object-level statements"),
- ("iprover", iprover_meth, "intuitionistic proof search"),
- ("rule", thms_ctxt_args some_rule, "apply some intro/elim rule"),
- ("erule", nat_thms_args erule, "apply rule in elimination manner (improper)"),
- ("drule", nat_thms_args drule, "apply rule in destruct manner (improper)"),
- ("frule", nat_thms_args frule, "apply rule in forward manner (improper)"),
- ("this", no_args this, "apply current facts as rules"),
- ("fact", thms_ctxt_args fact, "composition by facts from context"),
- ("assumption", ctxt_args assumption, "proof by assumption, preferring facts"),
- ("rename_tac", goal_args (Scan.repeat1 Args.name) Tactic.rename_params_tac,
- "rename parameters of goal"),
- ("rotate_tac", goal_args (Scan.optional Args.int 1) Tactic.rotate_tac,
- "rotate assumptions of goal"),
- ("tactic", simple_args (Args.position Args.name) tactic, "ML tactic as proof method"),
- ("raw_tactic", simple_args (Args.position Args.name) raw_tactic, "ML tactic as raw proof method")]);
+val _ = Context.>> (Context.map_theory
+ (add_methods
+ [("fail", no_args fail, "force failure"),
+ ("succeed", no_args succeed, "succeed"),
+ ("-", no_args insert_facts, "do nothing (insert current facts only)"),
+ ("insert", thms_args insert, "insert theorems, ignoring facts (improper)"),
+ ("intro", thms_args intro, "repeatedly apply introduction rules"),
+ ("elim", thms_args elim, "repeatedly apply elimination rules"),
+ ("unfold", thms_ctxt_args unfold_meth, "unfold definitions"),
+ ("fold", thms_ctxt_args fold_meth, "fold definitions"),
+ ("atomize", (atomize o fst) oo syntax (Args.mode "full"),
+ "present local premises as object-level statements"),
+ ("iprover", iprover_meth, "intuitionistic proof search"),
+ ("rule", thms_ctxt_args some_rule, "apply some intro/elim rule"),
+ ("erule", nat_thms_args erule, "apply rule in elimination manner (improper)"),
+ ("drule", nat_thms_args drule, "apply rule in destruct manner (improper)"),
+ ("frule", nat_thms_args frule, "apply rule in forward manner (improper)"),
+ ("this", no_args this, "apply current facts as rules"),
+ ("fact", thms_ctxt_args fact, "composition by facts from context"),
+ ("assumption", ctxt_args assumption, "proof by assumption, preferring facts"),
+ ("rename_tac", goal_args (Scan.repeat1 Args.name) Tactic.rename_params_tac,
+ "rename parameters of goal"),
+ ("rotate_tac", goal_args (Scan.optional Args.int 1) Tactic.rotate_tac,
+ "rotate assumptions of goal"),
+ ("tactic", simple_args (Args.position Args.name) tactic, "ML tactic as proof method"),
+ ("raw_tactic", simple_args (Args.position Args.name) raw_tactic,
+ "ML tactic as raw proof method")]));
(* outer parser *)
--- a/src/Pure/Isar/object_logic.ML Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/Isar/object_logic.ML Fri Mar 28 20:02:04 2008 +0100
@@ -193,7 +193,7 @@
val declare_atomize = Thm.declaration_attribute (fn th => Context.mapping (add_atomize th) I);
val declare_rulify = Thm.declaration_attribute (fn th => Context.mapping (add_rulify th) I);
-val _ = Context.>> (add_rulify Drule.norm_hhf_eq);
+val _ = Context.>> (Context.map_theory (add_rulify Drule.norm_hhf_eq));
(* atomize *)
--- a/src/Pure/Isar/proof_context.ML Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/Isar/proof_context.ML Fri Mar 28 20:02:04 2008 +0100
@@ -571,9 +571,8 @@
fun standard_term_uncheck ctxt =
map (contract_abbrevs ctxt);
-fun add eq what f = Context.>>
- (Context.theory_map (what (fn xs => fn ctxt =>
- let val xs' = f ctxt xs in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end)));
+fun add eq what f = Context.>> (what (fn xs => fn ctxt =>
+ let val xs' = f ctxt xs in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end));
in
@@ -922,14 +921,14 @@
in
-val _ = Context.>>
+val _ = Context.>> (Context.map_theory
(Sign.add_syntax
[("_context_const", "id => 'a", Delimfix "CONST _"),
("_context_const", "longid => 'a", Delimfix "CONST _"),
("_context_xconst", "id => 'a", Delimfix "XCONST _"),
("_context_xconst", "longid => 'a", Delimfix "XCONST _")] #>
Sign.add_advanced_trfuns
- ([("_context_const", const_ast_tr true), ("_context_xconst", const_ast_tr false)], [], [], []));
+ ([("_context_const", const_ast_tr true), ("_context_xconst", const_ast_tr false)], [], [], [])));
end;
--- a/src/Pure/Isar/rule_insts.ML Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/Isar/rule_insts.ML Fri Mar 28 20:02:04 2008 +0100
@@ -218,9 +218,10 @@
(* setup *)
-val _ = Context.>> (Attrib.add_attributes
- [("where", where_att, "named instantiation of theorem"),
- ("of", of_att, "positional instantiation of theorem")]);
+val _ = Context.>> (Context.map_theory
+ (Attrib.add_attributes
+ [("where", where_att, "named instantiation of theorem"),
+ ("of", of_att, "positional instantiation of theorem")]));
@@ -367,21 +368,22 @@
(* setup *)
-val _ = Context.>> (Method.add_methods
- [("rule_tac", inst_args_var res_inst_meth,
- "apply rule (dynamic instantiation)"),
- ("erule_tac", inst_args_var eres_inst_meth,
- "apply rule in elimination manner (dynamic instantiation)"),
- ("drule_tac", inst_args_var dres_inst_meth,
- "apply rule in destruct manner (dynamic instantiation)"),
- ("frule_tac", inst_args_var forw_inst_meth,
- "apply rule in forward manner (dynamic instantiation)"),
- ("cut_tac", inst_args_var cut_inst_meth,
- "cut rule (dynamic instantiation)"),
- ("subgoal_tac", Method.goal_args_ctxt (Scan.repeat1 Args.name) subgoals_tac,
- "insert subgoal (dynamic instantiation)"),
- ("thin_tac", Method.goal_args_ctxt Args.name thin_tac,
- "remove premise (dynamic instantiation)")]);
+val _ = Context.>> (Context.map_theory
+ (Method.add_methods
+ [("rule_tac", inst_args_var res_inst_meth,
+ "apply rule (dynamic instantiation)"),
+ ("erule_tac", inst_args_var eres_inst_meth,
+ "apply rule in elimination manner (dynamic instantiation)"),
+ ("drule_tac", inst_args_var dres_inst_meth,
+ "apply rule in destruct manner (dynamic instantiation)"),
+ ("frule_tac", inst_args_var forw_inst_meth,
+ "apply rule in forward manner (dynamic instantiation)"),
+ ("cut_tac", inst_args_var cut_inst_meth,
+ "cut rule (dynamic instantiation)"),
+ ("subgoal_tac", Method.goal_args_ctxt (Scan.repeat1 Args.name) subgoals_tac,
+ "insert subgoal (dynamic instantiation)"),
+ ("thin_tac", Method.goal_args_ctxt Args.name thin_tac,
+ "remove premise (dynamic instantiation)")]));
end;
--- a/src/Pure/Isar/skip_proof.ML Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/Isar/skip_proof.ML Fri Mar 28 20:02:04 2008 +0100
@@ -24,7 +24,8 @@
if ! quick_and_dirty then prop
else error "Proof may be skipped in quick_and_dirty mode only!";
-val _ = Context.>> (Theory.add_oracle ("skip_proof", skip_proof));
+val _ = Context.>> (Context.map_theory
+ (Theory.add_oracle ("skip_proof", skip_proof)));
(* basic cheating *)
--- a/src/Pure/Proof/extraction.ML Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/Proof/extraction.ML Fri Mar 28 20:02:04 2008 +0100
@@ -395,7 +395,7 @@
(** Pure setup **)
-val _ = Context.>>
+val _ = Context.>> (Context.map_theory
(add_types [("prop", ([], NONE))] #>
add_typeof_eqns
@@ -441,7 +441,7 @@
Attrib.add_attributes
[("extraction_expand", extraction_expand,
- "specify theorems / definitions to be expanded during extraction")]);
+ "specify theorems / definitions to be expanded during extraction")]));
(**** extract program ****)
--- a/src/Pure/Proof/proof_rewrite_rules.ML Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Fri Mar 28 20:02:04 2008 +0100
@@ -187,7 +187,7 @@
in rew' end;
fun rprocs b = [("Pure/meta_equality", rew b)];
-val _ = Context.>> (fold Proofterm.add_prf_rproc (rprocs false));
+val _ = Context.>> (Context.map_theory (fold Proofterm.add_prf_rproc (rprocs false)));
(**** apply rewriting function to all terms in proof ****)
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Fri Mar 28 20:02:04 2008 +0100
@@ -92,7 +92,7 @@
in
-val _ = Context.>> (Sign.add_tokentrfuns proof_general_trans);
+val _ = Context.>> (Context.map_theory (Sign.add_tokentrfuns proof_general_trans));
end;
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Fri Mar 28 20:02:04 2008 +0100
@@ -105,7 +105,7 @@
in
-val _ = Context.>> (Sign.add_tokentrfuns proof_general_trans);
+val _ = Context.>> (Context.map_theory (Sign.add_tokentrfuns proof_general_trans));
end;
--- a/src/Pure/Thy/html.ML Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/Thy/html.ML Fri Mar 28 20:02:04 2008 +0100
@@ -267,7 +267,8 @@
("var", var_or_skolem),
("xstr", style "xstr")];
-val _ = Context.>> (Sign.add_mode_tokentrfuns htmlN html_trans);
+val _ = Context.>> (Context.map_theory
+ (Sign.add_mode_tokentrfuns htmlN html_trans));
--- a/src/Pure/Thy/term_style.ML Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/Thy/term_style.ML Fri Mar 28 20:02:04 2008 +0100
@@ -65,7 +65,7 @@
" in propositon: " ^ Syntax.string_of_term ctxt t)
end;
-val _ = Context.>>
+val _ = Context.>> (Context.map_theory
(add_style "lhs" (fst oo style_binargs) #>
add_style "rhs" (snd oo style_binargs) #>
add_style "prem1" (style_parm_premise 1) #>
@@ -87,6 +87,6 @@
add_style "prem17" (style_parm_premise 17) #>
add_style "prem18" (style_parm_premise 18) #>
add_style "prem19" (style_parm_premise 19) #>
- add_style "concl" (K Logic.strip_imp_concl));
+ add_style "concl" (K Logic.strip_imp_concl)));
end;
--- a/src/Pure/Tools/isabelle_process.ML Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/Tools/isabelle_process.ML Fri Mar 28 20:02:04 2008 +0100
@@ -160,7 +160,7 @@
in
-val _ = Context.>> (Sign.add_tokentrfuns token_trans);
+val _ = Context.>> (Context.map_theory (Sign.add_tokentrfuns token_trans));
end;
--- a/src/Pure/assumption.ML Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/assumption.ML Fri Mar 28 20:02:04 2008 +0100
@@ -79,8 +79,8 @@
(* named prems -- legacy feature *)
val _ = Context.>>
- (PureThy.add_thms_dynamic ("prems",
- fn Context.Theory _ => [] | Context.Proof ctxt => prems_of ctxt));
+ (Context.map_theory (PureThy.add_thms_dynamic ("prems",
+ fn Context.Theory _ => [] | Context.Proof ctxt => prems_of ctxt)));
(* add assumptions *)
--- a/src/Pure/codegen.ML Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/codegen.ML Fri Mar 28 20:02:04 2008 +0100
@@ -343,8 +343,8 @@
(let
fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
in
- Code.add_attribute ("unfold", Scan.succeed (mk_attribute
- (fn thm => add_unfold thm #> Code.add_inline thm)))
+ Context.map_theory (Code.add_attribute ("unfold", Scan.succeed (mk_attribute
+ (fn thm => add_unfold thm #> Code.add_inline thm))))
end);
@@ -786,9 +786,9 @@
(add_edge (node_id, dep) gr'', p module''))
end);
-val _ = Context.>>
+val _ = Context.>> (Context.map_theory
(add_codegen "default" default_codegen #>
- add_tycodegen "default" default_tycodegen);
+ add_tycodegen "default" default_tycodegen));
fun mk_tuple [p] = p
@@ -1026,8 +1026,7 @@
else state
end;
-val _ = Context.>>
- (Context.theory_map (Specification.add_theorem_hook test_goal'));
+val _ = Context.>> (Specification.add_theorem_hook test_goal');
(**** Evaluator for terms ****)
@@ -1078,8 +1077,8 @@
let val {thy, t, ...} = rep_cterm ct
in Thm.invoke_oracle_i thy "Pure.evaluation" (thy, Evaluation t) end;
-val _ = Context.>>
- (Theory.add_oracle ("evaluation", evaluation_oracle));
+val _ = Context.>> (Context.map_theory
+ (Theory.add_oracle ("evaluation", evaluation_oracle)));
(**** Interface ****)
--- a/src/Pure/compress.ML Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/compress.ML Fri Mar 28 20:02:04 2008 +0100
@@ -30,7 +30,7 @@
ref (Termtab.merge (K true) (terms1, terms2)));
);
-val _ = Context.>> CompressData.init;
+val _ = Context.>> (Context.map_theory CompressData.init);
(* compress types *)
--- a/src/Pure/context.ML Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/context.ML Fri Mar 28 20:02:04 2008 +0100
@@ -66,8 +66,8 @@
val the_thread_data: unit -> generic
val set_thread_data: generic option -> unit
val setmp_thread_data: generic option -> ('a -> 'b) -> 'a -> 'b
- val >> : (theory -> theory) -> unit
- val >>> : (theory -> 'a * theory) -> 'a
+ val >> : (generic -> generic) -> unit
+ val >>> : (generic -> 'a * generic) -> 'a
end;
signature PRIVATE_CONTEXT =
@@ -525,12 +525,12 @@
fun >>> f =
let
- val (res, thy') = f (the_theory (the_thread_data ()));
- val _ = set_thread_data (SOME (Theory thy'));
+ val (res, context') = f (the_thread_data ());
+ val _ = set_thread_data (SOME context');
in res end;
nonfix >>;
-fun >> f = >>> (fn thy => ((), f thy));
+fun >> f = >>> (fn context => ((), f context));
val _ = set_thread_data (SOME (Theory pre_pure_thy));
--- a/src/Pure/pure_setup.ML Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/pure_setup.ML Fri Mar 28 20:02:04 2008 +0100
@@ -16,8 +16,9 @@
(* the Pure theories *)
-Context.>> (OuterSyntax.process_file (Path.explode "Pure.thy"));
-Context.>> Theory.end_theory;
+Context.>> (Context.map_theory
+ (OuterSyntax.process_file (Path.explode "Pure.thy") #>
+ Theory.end_theory));
structure Pure = struct val thy = ML_Context.the_global_context () end;
Context.set_thread_data NONE;
ThyInfo.register_theory Pure.thy;
--- a/src/Pure/pure_thy.ML Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/pure_thy.ML Fri Mar 28 20:02:04 2008 +0100
@@ -146,7 +146,7 @@
ref (make_thms NameSpace.empty_table (Facts.merge (all_facts1, all_facts2)));
);
-val _ = Context.>> TheoremsData.init;
+val _ = Context.>> (Context.map_theory TheoremsData.init);
val get_theorems_ref = TheoremsData.get;
val get_theorems = (fn Thms args => args) o ! o get_theorems_ref;
@@ -423,7 +423,7 @@
val term = SimpleSyntax.read_term;
val prop = SimpleSyntax.read_prop;
-val _ = Context.>>
+val _ = Context.>> (Context.map_theory
(Sign.add_types
[("fun", 2, NoSyn),
("prop", 0, NoSyn),
@@ -515,7 +515,7 @@
("conjunction_def", prop "(A && B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd
#> Sign.hide_consts false ["conjunction", "term"]
#> add_thmss [(("nothing", []), [])] #> snd
- #> Theory.add_axioms_i Proofterm.equality_axms);
+ #> Theory.add_axioms_i Proofterm.equality_axms));
end;
--- a/src/Pure/simplifier.ML Fri Mar 28 19:43:54 2008 +0100
+++ b/src/Pure/simplifier.ML Fri Mar 28 20:02:04 2008 +0100
@@ -105,7 +105,7 @@
fun merge _ (ref ss1, ref ss2) = ref (merge_ss (ss1, ss2));
);
-val _ = Context.>> GlobalSimpset.init;
+val _ = Context.>> (Context.map_theory GlobalSimpset.init);
fun print_simpset thy = print_ss (! (GlobalSimpset.get thy));
val get_simpset = ! o GlobalSimpset.get;
@@ -369,12 +369,12 @@
(* setup attributes *)
-val _ = Context.>>
+val _ = Context.>> (Context.map_theory
(Attrib.add_attributes
[(simpN, Attrib.add_del_args simp_add simp_del, "declaration of Simplifier rewrite rule"),
(congN, Attrib.add_del_args cong_add cong_del, "declaration of Simplifier congruence rule"),
("simproc", simproc_att, "declaration of simplification procedures"),
- ("simplified", simplified, "simplified rule")]);
+ ("simplified", simplified, "simplified rule")]));