--- a/src/HOL/Import/import_data.ML Fri Aug 23 20:09:34 2013 +0200
+++ b/src/HOL/Import/import_data.ML Fri Aug 23 20:35:50 2013 +0200
@@ -90,16 +90,16 @@
val parser = Parse.name -- Scan.option (Parse.$$$ ":" |-- Parse.xname)
fun add_const_attr (s1, s2) = Thm.declaration_attribute
(fn th => Context.mapping (add_const_def s1 th s2) (fn x => x))
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(Attrib.setup (Binding.name "import_const") (Scan.lift parser >> add_const_attr)
- "Declare a theorem as an equality that maps the given constant"))
+ "Declare a theorem as an equality that maps the given constant")
val parser = Parse.name -- (Parse.name -- Parse.name)
fun add_typ_attr (tyname, (absname, repname)) = Thm.declaration_attribute
(fn th => Context.mapping (add_typ_def tyname absname repname th) (fn x => x))
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(Attrib.setup (Binding.name "import_type") (Scan.lift parser >> add_typ_attr)
- "Declare a type_definion theorem as a map for an imported type abs rep"))
+ "Declare a type_definion theorem as a map for an imported type abs rep")
val type_map = (Parse.name --| Parse.$$$ ":" -- Parse.xname) >>
(fn (ty_name1, ty_name2) => add_typ_map ty_name1 ty_name2)
@@ -115,11 +115,11 @@
(* Initial type and constant maps, for types and constants that are not
defined, which means their definitions do not appear in the proof dump *)
-val _ = Context.>> (Context.map_theory (
+val _ = Theory.setup
add_typ_map "bool" @{type_name bool} o
add_typ_map "fun" @{type_name fun} o
add_typ_map "ind" @{type_name ind} o
add_const_map "=" @{const_name HOL.eq} o
- add_const_map "@" @{const_name "Eps"}))
+ add_const_map "@" @{const_name "Eps"})
end
--- a/src/HOL/Tools/reflection.ML Fri Aug 23 20:09:34 2013 +0200
+++ b/src/HOL/Tools/reflection.ML Fri Aug 23 20:35:50 2013 +0200
@@ -65,11 +65,13 @@
val add_correctness_thm = Thm.declaration_attribute (Data.map o apsnd o Thm.add_thm);
val del_correctness_thm = Thm.declaration_attribute (Data.map o apsnd o Thm.del_thm);
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(Attrib.setup @{binding reify}
- (Attrib.add_del add_reification_eq del_reification_eq) "declare reification equations" #>
- Attrib.setup @{binding reflection}
- (Attrib.add_del add_correctness_thm del_correctness_thm) "declare reflection correctness theorems"));
+ (Attrib.add_del add_reification_eq del_reification_eq)
+ "declare reification equations" #>
+ Attrib.setup @{binding reflection}
+ (Attrib.add_del add_correctness_thm del_correctness_thm)
+ "declare reflection correctness theorems");
fun default_reify_tac ctxt user_eqs =
let
--- a/src/Pure/Isar/attrib.ML Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/Isar/attrib.ML Fri Aug 23 20:35:50 2013 +0200
@@ -385,7 +385,7 @@
(* theory setup *)
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(setup (Binding.name "attribute") (Scan.lift Args.internal_attribute >> Morphism.form)
"internal attribute" #>
setup (Binding.name "tagged") (Scan.lift (Args.name -- Args.name) >> Thm.tag) "tagged theorem" #>
@@ -427,7 +427,7 @@
setup (Binding.name "abs_def")
(Scan.succeed (Thm.rule_attribute (fn context =>
Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def)))
- "abstract over free variables of definitional theorem"));
+ "abstract over free variables of definitional theorem");
@@ -506,7 +506,7 @@
fun setup_config declare_config binding default =
let
val (config, setup) = declare_config binding default;
- val _ = Context.>> (Context.map_theory setup);
+ val _ = Theory.setup setup;
in config end;
in
@@ -531,7 +531,7 @@
fun setup_option coerce name =
let
val config = Config.declare_option name;
- val _ = Context.>> (Context.map_theory (register_config config));
+ val _ = Theory.setup (register_config config);
in coerce config end;
in
@@ -551,7 +551,7 @@
(* theory setup *)
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(register_config quick_and_dirty_raw #>
register_config Ast.trace_raw #>
register_config Ast.stats_raw #>
@@ -582,6 +582,6 @@
register_config Raw_Simplifier.simp_depth_limit_raw #>
register_config Raw_Simplifier.simp_trace_depth_limit_raw #>
register_config Raw_Simplifier.simp_debug_raw #>
- register_config Raw_Simplifier.simp_trace_raw));
+ register_config Raw_Simplifier.simp_trace_raw);
end;
--- a/src/Pure/Isar/calculation.ML Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/Isar/calculation.ML Fri Aug 23 20:35:50 2013 +0200
@@ -94,7 +94,7 @@
(* concrete syntax *)
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(Attrib.setup (Binding.name "trans") (Attrib.add_del trans_add trans_del)
"declaration of transitivity rule" #>
Attrib.setup (Binding.name "sym") (Attrib.add_del sym_add sym_del)
@@ -103,7 +103,7 @@
"resolution with symmetry rule" #>
Global_Theory.add_thms
[((Binding.empty, transitive_thm), [trans_add]),
- ((Binding.empty, symmetric_thm), [sym_add])] #> snd));
+ ((Binding.empty, symmetric_thm), [sym_add])] #> snd);
--- a/src/Pure/Isar/class.ML Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/Isar/class.ML Fri Aug 23 20:35:50 2013 +0200
@@ -659,11 +659,11 @@
HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
default_intro_tac ctxt facts;
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(Method.setup (Binding.name "intro_classes") (Scan.succeed (K (METHOD intro_classes_tac)))
"back-chain introduction rules of classes" #>
Method.setup (Binding.name "default") (Attrib.thms >> (METHOD oo default_tac))
- "apply some intro/elim rule"));
+ "apply some intro/elim rule");
end;
--- a/src/Pure/Isar/code.ML Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/Isar/code.ML Fri Aug 23 20:35:50 2013 +0200
@@ -320,9 +320,8 @@
#> map_history_concluded (K true))
|> SOME;
-val _ =
- Context.>> (Context.map_theory
- (Theory.at_begin continue_history #> Theory.at_end conclude_history));
+val _ = Theory.setup
+ (Theory.at_begin continue_history #> Theory.at_end conclude_history);
(* access to data dependent on abstract executable code *)
@@ -1233,7 +1232,7 @@
(* setup *)
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(let
fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
val code_attribute_parser =
@@ -1247,7 +1246,7 @@
Datatype_Interpretation.init
#> Attrib.setup (Binding.name "code") (Scan.lift code_attribute_parser)
"declare theorems for code generation"
- end));
+ end);
end; (*struct*)
--- a/src/Pure/Isar/context_rules.ML Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/Isar/context_rules.ML Fri Aug 23 20:35:50 2013 +0200
@@ -198,8 +198,8 @@
val elim_query = rule_add elim_queryK I;
val dest_query = rule_add elim_queryK Tactic.make_elim;
-val _ = Context.>> (Context.map_theory
- (snd o Global_Theory.add_thms [((Binding.empty, Drule.equal_intr_rule), [intro_query NONE])]));
+val _ = Theory.setup
+ (snd o Global_Theory.add_thms [((Binding.empty, Drule.equal_intr_rule), [intro_query NONE])]);
(* concrete syntax *)
@@ -208,7 +208,7 @@
(Scan.lift ((Args.bang >> K a || Args.query >> K c || Scan.succeed b) --
Scan.option Parse.nat) >> (fn (f, n) => f n)) x;
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(Attrib.setup (Binding.name "intro") (add intro_bang intro intro_query)
"declaration of introduction rule" #>
Attrib.setup (Binding.name "elim") (add elim_bang elim elim_query)
@@ -216,6 +216,6 @@
Attrib.setup (Binding.name "dest") (add dest_bang dest dest_query)
"declaration of destruction rule" #>
Attrib.setup (Binding.name "rule") (Scan.lift Args.del >> K rule_del)
- "remove declaration of intro/elim/dest rule"));
+ "remove declaration of intro/elim/dest rule");
end;
--- a/src/Pure/Isar/isar_cmd.ML Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Fri Aug 23 20:35:50 2013 +0200
@@ -265,12 +265,11 @@
Proof.goal (Toplevel.proof_of (diag_state ctxt))
handle Toplevel.UNDEF => error "No goal present";
-val _ =
- Context.>> (Context.map_theory
- (ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "state"))
- (Scan.succeed "Isar_Cmd.diag_state ML_context") #>
- ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "goal"))
- (Scan.succeed "Isar_Cmd.diag_goal ML_context")));
+val _ = Theory.setup
+ (ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "state"))
+ (Scan.succeed "Isar_Cmd.diag_state ML_context") #>
+ ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "goal"))
+ (Scan.succeed "Isar_Cmd.diag_goal ML_context"));
(* print theorems *)
--- a/src/Pure/Isar/locale.ML Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/Isar/locale.ML Fri Aug 23 20:35:50 2013 +0200
@@ -613,11 +613,11 @@
val intro_locales_tac = gen_intro_locales_tac Method.intros_tac;
val try_intro_locales_tac= gen_intro_locales_tac Method.try_intros_tac;
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(Method.setup (Binding.name "intro_locales") (Scan.succeed (METHOD o try_intro_locales_tac false))
"back-chain introduction rules of locales without unfolding predicates" #>
Method.setup (Binding.name "unfold_locales") (Scan.succeed (METHOD o try_intro_locales_tac true))
- "back-chain all introduction rules of locales"));
+ "back-chain all introduction rules of locales");
(*** diagnostic commands and interfaces ***)
--- a/src/Pure/Isar/method.ML Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/Isar/method.ML Fri Aug 23 20:35:50 2013 +0200
@@ -438,7 +438,7 @@
(* theory setup *)
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(setup (Binding.name "fail") (Scan.succeed (K fail)) "force failure" #>
setup (Binding.name "succeed") (Scan.succeed (K succeed)) "succeed" #>
setup (Binding.name "-") (Scan.succeed (K insert_facts))
@@ -470,7 +470,7 @@
setup (Binding.name "tactic") (Scan.lift Args.name_source_position >> tactic)
"ML tactic as proof method" #>
setup (Binding.name "raw_tactic") (Scan.lift Args.name_source_position >> raw_tactic)
- "ML tactic as raw proof method"));
+ "ML tactic as raw proof method");
(*final declarations of this structure!*)
--- a/src/Pure/Isar/object_logic.ML Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/Isar/object_logic.ML Fri Aug 23 20:35:50 2013 +0200
@@ -174,7 +174,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.>> (Context.map_theory (fold add_rulify Drule.norm_hhf_eqs));
+val _ = Theory.setup (fold add_rulify Drule.norm_hhf_eqs);
(* atomize *)
--- a/src/Pure/Isar/rule_insts.ML Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/Isar/rule_insts.ML Fri Aug 23 20:35:50 2013 +0200
@@ -163,12 +163,12 @@
(* where: named instantiation *)
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(Attrib.setup (Binding.name "where")
(Scan.lift (Parse.and_list (Args.var -- (Args.$$$ "=" |-- Args.name_source))) >>
(fn args =>
Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args)))
- "named instantiation of theorem"));
+ "named instantiation of theorem");
(* of: positional instantiation (terms only) *)
@@ -184,11 +184,11 @@
in
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(Attrib.setup (Binding.name "of")
(Scan.lift insts >> (fn args =>
Thm.rule_attribute (fn context => read_instantiate_mixed' (Context.proof_of context) args)))
- "positional instantiation of theorem"));
+ "positional instantiation of theorem");
end;
@@ -341,7 +341,7 @@
(* setup *)
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(Method.setup (Binding.name "rule_tac") res_inst_meth "apply rule (dynamic instantiation)" #>
Method.setup (Binding.name "erule_tac") eres_inst_meth
"apply rule in elimination manner (dynamic instantiation)" #>
@@ -358,7 +358,7 @@
Method.setup (Binding.name "thin_tac")
(Args.goal_spec -- Scan.lift Args.name_source >>
(fn (quant, prop) => fn ctxt => SIMPLE_METHOD'' quant (thin_tac ctxt prop)))
- "remove premise (dynamic instantiation)"));
+ "remove premise (dynamic instantiation)");
end;
--- a/src/Pure/ML/ml_antiquote.ML Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/ML/ml_antiquote.ML Fri Aug 23 20:35:50 2013 +0200
@@ -54,8 +54,7 @@
(** misc antiquotations **)
-val _ = Context.>> (Context.map_theory
-
+val _ = Theory.setup
(inline (Binding.name "assert")
(Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
@@ -102,7 +101,7 @@
(Args.context --
Scan.lift Args.name_source >> uncurry Proof_Context.read_term_pattern >> (fn t =>
"Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
- ML_Syntax.atomic (ML_Syntax.print_term t)))));
+ ML_Syntax.atomic (ML_Syntax.print_term t))));
(* type classes *)
@@ -112,13 +111,13 @@
|> syn ? Lexicon.mark_class
|> ML_Syntax.print_string);
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(inline (Binding.name "class") (class false) #>
inline (Binding.name "class_syntax") (class true) #>
inline (Binding.name "sort")
(Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) =>
- ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))))));
+ ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))));
(* type constructors *)
@@ -134,7 +133,7 @@
| NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.here pos));
in ML_Syntax.print_string res end);
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(inline (Binding.name "type_name")
(type_name "logical type" (fn (c, Type.LogicalType _) => c)) #>
inline (Binding.name "type_abbrev")
@@ -142,7 +141,7 @@
inline (Binding.name "nonterminal")
(type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #>
inline (Binding.name "type_syntax")
- (type_name "type" (fn (c, _) => Lexicon.mark_type c))));
+ (type_name "type" (fn (c, _) => Lexicon.mark_type c)));
(* constants *)
@@ -155,7 +154,7 @@
handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
in ML_Syntax.print_string res end);
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(inline (Binding.name "const_name")
(const_name (fn (consts, c) => (Consts.the_const consts c; c))) #>
inline (Binding.name "const_abbrev")
@@ -181,7 +180,7 @@
error ("Constant requires " ^ string_of_int n ^ " type argument(s): " ^
quote c ^ enclose "(" ")" (commas (replicate n "_")));
val const = Const (c, Consts.instance consts (c, Ts));
- in ML_Syntax.atomic (ML_Syntax.print_term const) end))));
+ in ML_Syntax.atomic (ML_Syntax.print_term const) end)));
(* outer syntax *)
@@ -191,7 +190,7 @@
(f ((name, Thy_Header.the_keyword thy name), pos)
handle ERROR msg => error (msg ^ Position.here pos)));
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(value (Binding.name "keyword")
(with_keyword
(fn ((name, NONE), _) => "Parse.$$$ " ^ ML_Syntax.print_string name
@@ -209,7 +208,7 @@
(ML_Syntax.print_list ML_Syntax.print_string)))
ML_Syntax.print_position) ((name, kind), pos))
| ((name, NONE), pos) =>
- error ("Expected command keyword " ^ quote name ^ Position.here pos)))));
+ error ("Expected command keyword " ^ quote name ^ Position.here pos))));
end;
--- a/src/Pure/ML/ml_context.ML Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/ML/ml_context.ML Fri Aug 23 20:35:50 2013 +0200
@@ -74,7 +74,7 @@
let
val ths' = Context.>>> (Context.map_theory_result
(Global_Theory.store_thms (Binding.name name, ths)));
- val _ = Context.>> (Context.map_theory (Stored_Thms.put ths'));
+ val _ = Theory.setup (Stored_Thms.put ths');
val _ =
if name = "" then ()
else if not (ML_Syntax.is_identifier name) then
@@ -82,7 +82,7 @@
else
ML_Compiler.eval true Position.none
(ML_Lex.tokenize ("val " ^ name ^ " = " ^ get ^ " ();"));
- val _ = Context.>> (Context.map_theory (Stored_Thms.put []));
+ val _ = Theory.setup (Stored_Thms.put []);
in () end;
val ml_store_thms = ml_store "ML_Context.get_stored_thms";
--- a/src/Pure/ML/ml_thms.ML Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/ML/ml_thms.ML Fri Aug 23 20:35:50 2013 +0200
@@ -34,23 +34,22 @@
(* attribute source *)
-val _ =
- Context.>> (Context.map_theory
- (ML_Context.add_antiq (Binding.name "attributes")
- (Scan.depend (fn context => Parse_Spec.attribs >> (fn raw_srcs =>
- let
- val ctxt = Context.the_proof context;
- val thy = Proof_Context.theory_of ctxt;
+val _ = Theory.setup
+ (ML_Context.add_antiq (Binding.name "attributes")
+ (Scan.depend (fn context => Parse_Spec.attribs >> (fn raw_srcs =>
+ let
+ val ctxt = Context.the_proof context;
+ val thy = Proof_Context.theory_of ctxt;
- val i = serial ();
- val srcs = map (Attrib.intern_src thy) raw_srcs;
- val _ = map (Attrib.attribute ctxt) srcs;
- val (a, ctxt') = ctxt
- |> ML_Antiquote.variant "attributes" ||> put_attributes (i, srcs);
- val ml =
- ("val " ^ a ^ " = ML_Thms.the_attributes ML_context " ^
- string_of_int i ^ ";\n", "Isabelle." ^ a);
- in (Context.Proof ctxt', K ml) end)))));
+ val i = serial ();
+ val srcs = map (Attrib.intern_src thy) raw_srcs;
+ val _ = map (Attrib.attribute ctxt) srcs;
+ val (a, ctxt') = ctxt
+ |> ML_Antiquote.variant "attributes" ||> put_attributes (i, srcs);
+ val ml =
+ ("val " ^ a ^ " = ML_Thms.the_attributes ML_context " ^
+ string_of_int i ^ ";\n", "Isabelle." ^ a);
+ in (Context.Proof ctxt', K ml) end))));
(* fact references *)
@@ -73,14 +72,13 @@
else ("", ml_body);
in (Context.Proof ctxt'', decl) end;
-val _ =
- Context.>> (Context.map_theory
- (ML_Context.add_antiq (Binding.name "thm")
- (Scan.depend (fn context =>
- Scan.pass context Attrib.thm >> (thm_binding "thm" true context o single))) #>
- ML_Context.add_antiq (Binding.name "thms")
- (Scan.depend (fn context =>
- Scan.pass context Attrib.thms >> thm_binding "thms" false context))));
+val _ = Theory.setup
+ (ML_Context.add_antiq (Binding.name "thm")
+ (Scan.depend (fn context =>
+ Scan.pass context Attrib.thm >> (thm_binding "thm" true context o single))) #>
+ ML_Context.add_antiq (Binding.name "thms")
+ (Scan.depend (fn context =>
+ Scan.pass context Attrib.thms >> thm_binding "thms" false context)));
(* ad-hoc goals *)
@@ -89,9 +87,8 @@
val by = Args.$$$ "by";
val goal = Scan.unless (by || and_) Args.name_source;
-val _ =
- Context.>> (Context.map_theory
- (ML_Context.add_antiq (Binding.name "lemma")
+val _ = Theory.setup
+ (ML_Context.add_antiq (Binding.name "lemma")
(Scan.depend (fn context =>
Args.mode "open" -- Parse.and_list1 (Scan.repeat1 goal) --
(by |-- Method.parse -- Scan.option Method.parse) >>
@@ -111,7 +108,7 @@
val thms =
Proof_Context.get_fact ctxt'
(Facts.named (Proof_Context.full_name ctxt' (Binding.name Auto_Bind.thisN)));
- in thm_binding "lemma" (length (flat propss) = 1) context thms end)))));
+ in thm_binding "lemma" (length (flat propss) = 1) context thms end))));
end;
--- a/src/Pure/Proof/extraction.ML Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/Proof/extraction.ML Fri Aug 23 20:35:50 2013 +0200
@@ -422,7 +422,7 @@
(** Pure setup **)
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(add_types [("prop", ([], NONE))] #>
add_typeof_eqns
@@ -469,7 +469,7 @@
Attrib.setup (Binding.name "extraction_expand") (Scan.succeed (extraction_expand false))
"specify theorems to be expanded during extraction" #>
Attrib.setup (Binding.name "extraction_expand_def") (Scan.succeed (extraction_expand true))
- "specify definitions to be expanded during extraction"));
+ "specify definitions to be expanded during extraction");
(**** extract program ****)
--- a/src/Pure/Proof/proof_rewrite_rules.ML Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Fri Aug 23 20:35:50 2013 +0200
@@ -190,7 +190,7 @@
in rew' #> Option.map (rpair Proofterm.no_skel) end;
fun rprocs b = [rew b];
-val _ = Context.>> (Context.map_theory (fold Proofterm.add_prf_rproc (rprocs false)));
+val _ = Theory.setup (fold Proofterm.add_prf_rproc (rprocs false));
(**** apply rewriting function to all terms in proof ****)
--- a/src/Pure/Syntax/syntax_phases.ML Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Fri Aug 23 20:35:50 2013 +0200
@@ -807,14 +807,14 @@
(* setup translations *)
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(Sign.parse_ast_translation
[("_context_const", const_ast_tr true),
("_context_xconst", const_ast_tr false)] #>
Sign.typed_print_translation
[("_type_prop", type_prop_tr'),
("\\<^const>TYPE", type_tr'),
- ("_type_constraint_", type_constraint_tr')]));
+ ("_type_constraint_", type_constraint_tr')]);
--- a/src/Pure/Thy/present.ML Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/Thy/present.ML Fri Aug 23 20:35:50 2013 +0200
@@ -52,8 +52,8 @@
fun merge _ = empty;
);
-val _ = Context.>> (Context.map_theory
- (Browser_Info.put {chapter = Context.PureN, name = Context.PureN}));
+val _ = Theory.setup
+ (Browser_Info.put {chapter = Context.PureN, name = Context.PureN});
val session_name = #name o Browser_Info.get;
val session_chapter_name = (fn {chapter, name} => [chapter, name]) o Browser_Info.get;
--- a/src/Pure/Thy/rail.ML Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/Thy/rail.ML Fri Aug 23 20:35:50 2013 +0200
@@ -263,11 +263,10 @@
in
-val _ =
- Context.>> (Context.map_theory
- (Thy_Output.antiquotation (Binding.name "rail")
- (Scan.lift (Parse.source_position Parse.string))
- (fn {state, ...} => output_rules state o read)));
+val _ = Theory.setup
+ (Thy_Output.antiquotation (Binding.name "rail")
+ (Scan.lift (Parse.source_position Parse.string))
+ (fn {state, ...} => output_rules state o read));
end;
--- a/src/Pure/Thy/term_style.ML Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/Thy/term_style.ML Fri Aug 23 20:35:50 2013 +0200
@@ -91,11 +91,11 @@
| sub_term (Abs (n, T, b)) = Abs (sub_name n, T, sub_term b)
| sub_term t = t;
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(setup "lhs" (style_lhs_rhs fst) #>
setup "rhs" (style_lhs_rhs snd) #>
setup "prem" style_prem #>
setup "concl" (Scan.succeed (K Logic.strip_imp_concl)) #>
- setup "sub" (Scan.succeed (K sub_term))));
+ setup "sub" (Scan.succeed (K sub_term)));
end;
--- a/src/Pure/Thy/thy_load.ML Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/Thy/thy_load.ML Fri Aug 23 20:35:50 2013 +0200
@@ -275,9 +275,8 @@
(* document antiquotation *)
-val _ =
- Context.>> (Context.map_theory
- (Thy_Output.antiquotation (Binding.name "file") (Scan.lift (Parse.position Parse.path))
+val _ = Theory.setup
+ (Thy_Output.antiquotation (Binding.name "file") (Scan.lift (Parse.position Parse.path))
(fn {context = ctxt, ...} => fn (name, pos) =>
let
val dir = master_directory (Proof_Context.theory_of ctxt);
@@ -290,7 +289,7 @@
space_explode "/" name
|> map Thy_Output.verb_text
|> space_implode (Thy_Output.verb_text "/" ^ "\\discretionary{}{}{}")
- end)));
+ end));
(* global master path *)
--- a/src/Pure/Thy/thy_output.ML Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/Thy/thy_output.ML Fri Aug 23 20:35:50 2013 +0200
@@ -442,25 +442,24 @@
(* options *)
-val _ =
- Context.>> (Context.map_theory
- (add_option (Binding.name "show_types") (Config.put show_types o boolean) #>
- add_option (Binding.name "show_sorts") (Config.put show_sorts o boolean) #>
- add_option (Binding.name "show_structs") (Config.put show_structs o boolean) #>
- add_option (Binding.name "show_question_marks") (Config.put show_question_marks o boolean) #>
- add_option (Binding.name "show_abbrevs") (Config.put show_abbrevs o boolean) #>
- add_option (Binding.name "names_long") (Config.put Name_Space.names_long o boolean) #>
- add_option (Binding.name "names_short") (Config.put Name_Space.names_short o boolean) #>
- add_option (Binding.name "names_unique") (Config.put Name_Space.names_unique o boolean) #>
- add_option (Binding.name "eta_contract") (Config.put Syntax_Trans.eta_contract o boolean) #>
- add_option (Binding.name "display") (Config.put display o boolean) #>
- add_option (Binding.name "break") (Config.put break o boolean) #>
- add_option (Binding.name "quotes") (Config.put quotes o boolean) #>
- add_option (Binding.name "mode") (add_wrapper o Print_Mode.with_modes o single) #>
- add_option (Binding.name "margin") (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer) #>
- add_option (Binding.name "indent") (Config.put indent o integer) #>
- add_option (Binding.name "source") (Config.put source o boolean) #>
- add_option (Binding.name "goals_limit") (Config.put Goal_Display.goals_limit o integer)));
+val _ = Theory.setup
+ (add_option (Binding.name "show_types") (Config.put show_types o boolean) #>
+ add_option (Binding.name "show_sorts") (Config.put show_sorts o boolean) #>
+ add_option (Binding.name "show_structs") (Config.put show_structs o boolean) #>
+ add_option (Binding.name "show_question_marks") (Config.put show_question_marks o boolean) #>
+ add_option (Binding.name "show_abbrevs") (Config.put show_abbrevs o boolean) #>
+ add_option (Binding.name "names_long") (Config.put Name_Space.names_long o boolean) #>
+ add_option (Binding.name "names_short") (Config.put Name_Space.names_short o boolean) #>
+ add_option (Binding.name "names_unique") (Config.put Name_Space.names_unique o boolean) #>
+ add_option (Binding.name "eta_contract") (Config.put Syntax_Trans.eta_contract o boolean) #>
+ add_option (Binding.name "display") (Config.put display o boolean) #>
+ add_option (Binding.name "break") (Config.put break o boolean) #>
+ add_option (Binding.name "quotes") (Config.put quotes o boolean) #>
+ add_option (Binding.name "mode") (add_wrapper o Print_Mode.with_modes o single) #>
+ add_option (Binding.name "margin") (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer) #>
+ add_option (Binding.name "indent") (Config.put indent o integer) #>
+ add_option (Binding.name "source") (Config.put source o boolean) #>
+ add_option (Binding.name "goals_limit") (Config.put Goal_Display.goals_limit o integer));
(* basic pretty printing *)
@@ -564,22 +563,21 @@
in
-val _ =
- Context.>> (Context.map_theory
- (basic_entities_style (Binding.name "thm") (Term_Style.parse -- Attrib.thms) pretty_thm_style #>
- basic_entity (Binding.name "prop") (Term_Style.parse -- Args.prop) pretty_term_style #>
- basic_entity (Binding.name "term") (Term_Style.parse -- Args.term) pretty_term_style #>
- basic_entity (Binding.name "term_type") (Term_Style.parse -- Args.term) pretty_term_typ #>
- basic_entity (Binding.name "typeof") (Term_Style.parse -- Args.term) pretty_term_typeof #>
- basic_entity (Binding.name "const") (Args.const_proper false) pretty_const #>
- basic_entity (Binding.name "abbrev") (Scan.lift Args.name_source) pretty_abbrev #>
- basic_entity (Binding.name "typ") Args.typ_abbrev Syntax.pretty_typ #>
- basic_entity (Binding.name "class") (Scan.lift Args.name_source) pretty_class #>
- basic_entity (Binding.name "type") (Scan.lift Args.name) pretty_type #>
- basic_entity (Binding.name "text") (Scan.lift Args.name) pretty_text #>
- basic_entities (Binding.name "prf") Attrib.thms (pretty_prf false) #>
- basic_entities (Binding.name "full_prf") Attrib.thms (pretty_prf true) #>
- basic_entity (Binding.name "theory") (Scan.lift (Parse.position Args.name)) pretty_theory));
+val _ = Theory.setup
+ (basic_entities_style (Binding.name "thm") (Term_Style.parse -- Attrib.thms) pretty_thm_style #>
+ basic_entity (Binding.name "prop") (Term_Style.parse -- Args.prop) pretty_term_style #>
+ basic_entity (Binding.name "term") (Term_Style.parse -- Args.term) pretty_term_style #>
+ basic_entity (Binding.name "term_type") (Term_Style.parse -- Args.term) pretty_term_typ #>
+ basic_entity (Binding.name "typeof") (Term_Style.parse -- Args.term) pretty_term_typeof #>
+ basic_entity (Binding.name "const") (Args.const_proper false) pretty_const #>
+ basic_entity (Binding.name "abbrev") (Scan.lift Args.name_source) pretty_abbrev #>
+ basic_entity (Binding.name "typ") Args.typ_abbrev Syntax.pretty_typ #>
+ basic_entity (Binding.name "class") (Scan.lift Args.name_source) pretty_class #>
+ basic_entity (Binding.name "type") (Scan.lift Args.name) pretty_type #>
+ basic_entity (Binding.name "text") (Scan.lift Args.name) pretty_text #>
+ basic_entities (Binding.name "prf") Attrib.thms (pretty_prf false) #>
+ basic_entities (Binding.name "full_prf") Attrib.thms (pretty_prf true) #>
+ basic_entity (Binding.name "theory") (Scan.lift (Parse.position Args.name)) pretty_theory);
end;
@@ -600,10 +598,9 @@
in
-val _ =
- Context.>> (Context.map_theory
- (goal_state (Binding.name "goals") true #>
- goal_state (Binding.name "subgoals") false));
+val _ = Theory.setup
+ (goal_state (Binding.name "goals") true #>
+ goal_state (Binding.name "subgoals") false);
end;
@@ -612,9 +609,8 @@
val _ = Keyword.define ("by", NONE); (*overlap with command category*)
-val _ =
- Context.>> (Context.map_theory
- (antiquotation (Binding.name "lemma")
+val _ = Theory.setup
+ (antiquotation (Binding.name "lemma")
(Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse -- Scan.option Method.parse))
(fn {source, context, ...} => fn (prop, methods) =>
let
@@ -624,7 +620,7 @@
val _ = context
|> Proof.theorem NONE (K I) [[(prop, [])]]
|> Proof.global_terminal_proof methods;
- in output context (maybe_pretty_source pretty_term context prop_src [prop]) end)));
+ in output context (maybe_pretty_source pretty_term context prop_src [prop]) end));
(* ML text *)
@@ -649,20 +645,19 @@
in
-val _ =
- Context.>> (Context.map_theory
- (ml_text (Binding.name "ML") (ml_enclose "fn _ => (" ");") #>
- ml_text (Binding.name "ML_op") (ml_enclose "fn _ => (op " ");") #>
- ml_text (Binding.name "ML_type") (ml_enclose "val _ = NONE : (" ") option;") #>
- ml_text (Binding.name "ML_struct")
- (ml_enclose "functor XXX() = struct structure XX = " " end;") #>
+val _ = Theory.setup
+ (ml_text (Binding.name "ML") (ml_enclose "fn _ => (" ");") #>
+ ml_text (Binding.name "ML_op") (ml_enclose "fn _ => (op " ");") #>
+ ml_text (Binding.name "ML_type") (ml_enclose "val _ = NONE : (" ") option;") #>
+ ml_text (Binding.name "ML_struct")
+ (ml_enclose "functor XXX() = struct structure XX = " " end;") #>
- ml_text (Binding.name "ML_functor") (* FIXME formal treatment of functor name (!?) *)
- (fn pos => fn txt =>
- ML_Lex.read Position.none ("ML_Env.check_functor " ^
- ML_Syntax.print_string (Symbol_Pos.content (Symbol_Pos.explode (txt, pos))))) #>
+ ml_text (Binding.name "ML_functor") (* FIXME formal treatment of functor name (!?) *)
+ (fn pos => fn txt =>
+ ML_Lex.read Position.none ("ML_Env.check_functor " ^
+ ML_Syntax.print_string (Symbol_Pos.content (Symbol_Pos.explode (txt, pos))))) #>
- ml_text (Binding.name "ML_text") (K (K []))));
+ ml_text (Binding.name "ML_text") (K (K [])));
end;
--- a/src/Pure/axclass.ML Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/axclass.ML Fri Aug 23 20:35:50 2013 +0200
@@ -264,9 +264,8 @@
else SOME (map_proven_arities (K arities') thy)
end;
-val _ = Context.>> (Context.map_theory
- (Theory.at_begin complete_classrels #>
- Theory.at_begin complete_arities));
+val _ = Theory.setup
+ (Theory.at_begin complete_classrels #> Theory.at_begin complete_arities);
val _ = Proofterm.install_axclass_proofs
{classrel_proof = Thm.proof_of oo the_classrel,
--- a/src/Pure/pure_thy.ML Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/pure_thy.ML Fri Aug 23 20:35:50 2013 +0200
@@ -56,7 +56,7 @@
val token_markers =
["_tfree", "_tvar", "_free", "_bound", "_loose", "_var", "_numeral", "_inner_string"];
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(Sign.map_naming (Name_Space.set_theory_name Context.PureN) #>
Old_Appl_Syntax.put false #>
Sign.add_types_global
@@ -221,6 +221,6 @@
#> Sign.hide_const false "Pure.conjunction"
#> Global_Theory.add_thmss [((Binding.name "nothing", []), [])] #> snd
#> fold (fn (a, prop) =>
- snd o Thm.add_axiom_global (Binding.name a, prop)) Proofterm.equality_axms));
+ snd o Thm.add_axiom_global (Binding.name a, prop)) Proofterm.equality_axms);
end;
--- a/src/Pure/simplifier.ML Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/simplifier.ML Fri Aug 23 20:35:50 2013 +0200
@@ -129,10 +129,10 @@
(* global simprocs *)
fun Addsimprocs args =
- Context.>> (Context.map_theory (map_theory_simpset (fn ctxt => ctxt addsimprocs args)));
+ Theory.setup (map_theory_simpset (fn ctxt => ctxt addsimprocs args));
fun Delsimprocs args =
- Context.>> (Context.map_theory (map_theory_simpset (fn ctxt => ctxt delsimprocs args)));
+ Theory.setup (map_theory_simpset (fn ctxt => ctxt delsimprocs args));
@@ -154,13 +154,11 @@
fun check_simproc ctxt = Name_Space.check (Context.Proof ctxt) (get_simprocs ctxt) #> #1;
val the_simproc = Name_Space.get o get_simprocs;
-val _ =
- Context.>> (Context.map_theory
- (ML_Antiquote.value (Binding.name "simproc")
- (Args.context -- Scan.lift (Parse.position Args.name)
- >> (fn (ctxt, name) =>
- "Simplifier.the_simproc ML_context " ^
- ML_Syntax.print_string (check_simproc ctxt name)))));
+val _ = Theory.setup
+ (ML_Antiquote.value (Binding.name "simproc")
+ (Args.context -- Scan.lift (Parse.position Args.name)
+ >> (fn (ctxt, name) =>
+ "Simplifier.the_simproc ML_context " ^ ML_Syntax.print_string (check_simproc ctxt name))));
(* define simprocs *)
@@ -327,14 +325,14 @@
(* setup attributes *)
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(Attrib.setup (Binding.name simpN) (Attrib.add_del simp_add simp_del)
"declaration of Simplifier rewrite rule" #>
Attrib.setup (Binding.name congN) (Attrib.add_del cong_add cong_del)
"declaration of Simplifier congruence rule" #>
Attrib.setup (Binding.name "simproc") simproc_att
"declaration of simplification procedures" #>
- Attrib.setup (Binding.name "simplified") simplified "simplified rule"));
+ Attrib.setup (Binding.name "simplified") simplified "simplified rule");
--- a/src/Pure/theory.ML Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Pure/theory.ML Fri Aug 23 20:35:50 2013 +0200
@@ -15,6 +15,7 @@
val merge: theory * theory -> theory
val merge_list: theory list -> theory
val requires: theory -> string -> string -> unit
+ val setup: (theory -> theory) -> unit
val get_markup: theory -> Markup.T
val axiom_space: theory -> Name_Space.T
val axiom_table: theory -> term Symtab.table
@@ -59,6 +60,8 @@
if exists (fn thy' => Context.theory_name thy' = name) (nodes_of thy) then ()
else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);
+fun setup f = Context.>> (Context.map_theory f);
+
(** datatype thy **)
--- a/src/Tools/Code/code_runtime.ML Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Tools/Code/code_runtime.ML Fri Aug 23 20:35:50 2013 +0200
@@ -51,14 +51,14 @@
datatype truth = Holds;
-val _ = Context.>> (Context.map_theory
+val _ = Theory.setup
(Code_Target.extend_target (target, (Code_ML.target_SML, K I))
#> Code_Target.set_printings (Code_Symbol.Type_Constructor (@{type_name prop},
[(target, SOME (0, (K o K o K) (Code_Printer.str s_truth)))]))
#> Code_Target.set_printings (Code_Symbol.Constant (@{const_name Code_Generator.holds},
[(target, SOME (Code_Printer.plain_const_syntax s_Holds))]))
#> Code_Target.add_reserved target this
- #> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"]));
+ #> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"]);
(*avoid further pervasive infix names*)
val trace = Unsynchronized.ref false;
@@ -345,10 +345,9 @@
(** Isar setup **)
-val _ =
- Context.>> (Context.map_theory
- (ML_Context.add_antiq @{binding code}
- (Scan.depend (fn context => Scan.pass context Args.term >> ml_code_antiq context))));
+val _ = Theory.setup
+ (ML_Context.add_antiq @{binding code}
+ (Scan.depend (fn context => Scan.pass context Args.term >> ml_code_antiq context)));
local
@@ -387,7 +386,7 @@
fun notify_val (string, value) =
let
val _ = #enterVal ML_Env.name_space (string, value);
- val _ = Context.>> ((Context.map_theory o Loaded_Values.map) (insert (op =) string));
+ val _ = Theory.setup (Loaded_Values.map (insert (op =) string));
in () end;
fun abort _ = error "Only value bindings allowed.";
--- a/src/Tools/Spec_Check/output_style.ML Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Tools/Spec_Check/output_style.ML Fri Aug 23 20:35:50 2013 +0200
@@ -78,6 +78,8 @@
{status = status, finish = finish}
end)
+val _ = Theory.setup perl_style;
+
(* CM style: meshes with CM output; highlighted in sml-mode *)
@@ -106,9 +108,6 @@
{status = K (), finish = finish}
end)
-
-(* setup *)
-
-val _ = Context.>> (Context.map_theory (perl_style #> cm_style));
+val _ = Theory.setup cm_style;
end
--- a/src/Tools/try.ML Fri Aug 23 20:09:34 2013 +0200
+++ b/src/Tools/try.ML Fri Aug 23 20:35:50 2013 +0200
@@ -142,7 +142,6 @@
(* hybrid tool setup *)
-fun tool_setup tool =
- (Context.>> (Context.map_theory (register_tool tool)); print_function tool)
+fun tool_setup tool = (Theory.setup (register_tool tool); print_function tool)
end;