--- a/src/Pure/Isar/class.ML Tue Mar 18 13:36:28 2014 +0100
+++ b/src/Pure/Isar/class.ML Tue Mar 18 15:29:58 2014 +0100
@@ -666,9 +666,9 @@
default_intro_tac ctxt facts;
val _ = Theory.setup
- (Method.setup (Binding.name "intro_classes") (Scan.succeed (K (METHOD intro_classes_tac)))
+ (Method.setup @{binding 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))
+ Method.setup @{binding default} (Attrib.thms >> (METHOD oo default_tac))
"apply some intro/elim rule");
end;
--- a/src/Pure/Isar/code.ML Tue Mar 18 13:36:28 2014 +0100
+++ b/src/Pure/Isar/code.ML Tue Mar 18 15:29:58 2014 +0100
@@ -1285,7 +1285,7 @@
|| Scan.succeed (mk_attribute add_eqn_maybe_abs);
in
Datatype_Interpretation.init
- #> Attrib.setup (Binding.name "code") (Scan.lift code_attribute_parser)
+ #> Attrib.setup @{binding code} (Scan.lift code_attribute_parser)
"declare theorems for code generation"
end);
--- a/src/Pure/Isar/context_rules.ML Tue Mar 18 13:36:28 2014 +0100
+++ b/src/Pure/Isar/context_rules.ML Tue Mar 18 15:29:58 2014 +0100
@@ -209,13 +209,13 @@
Scan.option Parse.nat) >> (fn (f, n) => f n)) x;
val _ = Theory.setup
- (Attrib.setup (Binding.name "intro") (add intro_bang intro intro_query)
+ (Attrib.setup @{binding intro} (add intro_bang intro intro_query)
"declaration of introduction rule" #>
- Attrib.setup (Binding.name "elim") (add elim_bang elim elim_query)
+ Attrib.setup @{binding elim} (add elim_bang elim elim_query)
"declaration of elimination rule" #>
- Attrib.setup (Binding.name "dest") (add dest_bang dest dest_query)
+ Attrib.setup @{binding dest} (add dest_bang dest dest_query)
"declaration of destruction rule" #>
- Attrib.setup (Binding.name "rule") (Scan.lift Args.del >> K rule_del)
+ Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del)
"remove declaration of intro/elim/dest rule");
end;
--- a/src/Pure/Isar/isar_cmd.ML Tue Mar 18 13:36:28 2014 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Tue Mar 18 15:29:58 2014 +0100
@@ -247,9 +247,9 @@
handle Toplevel.UNDEF => error "No goal present";
val _ = Theory.setup
- (ML_Antiquotation.value (Binding.qualify true "Isar" (Binding.name "state"))
+ (ML_Antiquotation.value (Binding.qualify true "Isar" @{binding state})
(Scan.succeed "Isar_Cmd.diag_state ML_context") #>
- ML_Antiquotation.value (Binding.qualify true "Isar" (Binding.name "goal"))
+ ML_Antiquotation.value (Binding.qualify true "Isar" @{binding goal})
(Scan.succeed "Isar_Cmd.diag_goal ML_context"));
--- a/src/Pure/Isar/locale.ML Tue Mar 18 13:36:28 2014 +0100
+++ b/src/Pure/Isar/locale.ML Tue Mar 18 15:29:58 2014 +0100
@@ -622,9 +622,9 @@
val try_intro_locales_tac= gen_intro_locales_tac Method.try_intros_tac;
val _ = Theory.setup
- (Method.setup (Binding.name "intro_locales") (Scan.succeed (METHOD o try_intro_locales_tac false))
+ (Method.setup @{binding 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))
+ Method.setup @{binding unfold_locales} (Scan.succeed (METHOD o try_intro_locales_tac true))
"back-chain all introduction rules of locales");
--- a/src/Pure/Isar/method.ML Tue Mar 18 13:36:28 2014 +0100
+++ b/src/Pure/Isar/method.ML Tue Mar 18 15:29:58 2014 +0100
@@ -201,7 +201,7 @@
(* rule etc. -- single-step refinements *)
-val rule_trace = Attrib.setup_config_bool (Binding.name "rule_trace") (fn _ => false);
+val rule_trace = Attrib.setup_config_bool @{binding rule_trace} (fn _ => false);
fun trace ctxt rules =
if Config.get ctxt rule_trace andalso not (null rules) then
@@ -478,38 +478,38 @@
(* theory setup *)
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))
+ (setup @{binding fail} (Scan.succeed (K fail)) "force failure" #>
+ setup @{binding succeed} (Scan.succeed (K succeed)) "succeed" #>
+ setup @{binding "-"} (Scan.succeed (K insert_facts))
"do nothing (insert current facts only)" #>
- setup (Binding.name "insert") (Attrib.thms >> (K o insert))
+ setup @{binding insert} (Attrib.thms >> (K o insert))
"insert theorems, ignoring facts (improper)" #>
- setup (Binding.name "intro") (Attrib.thms >> (K o intro))
+ setup @{binding intro} (Attrib.thms >> (K o intro))
"repeatedly apply introduction rules" #>
- setup (Binding.name "elim") (Attrib.thms >> (K o elim))
+ setup @{binding elim} (Attrib.thms >> (K o elim))
"repeatedly apply elimination rules" #>
- setup (Binding.name "unfold") (Attrib.thms >> unfold_meth) "unfold definitions" #>
- setup (Binding.name "fold") (Attrib.thms >> fold_meth) "fold definitions" #>
- setup (Binding.name "atomize") (Scan.lift (Args.mode "full") >> atomize)
+ setup @{binding unfold} (Attrib.thms >> unfold_meth) "unfold definitions" #>
+ setup @{binding fold} (Attrib.thms >> fold_meth) "fold definitions" #>
+ setup @{binding atomize} (Scan.lift (Args.mode "full") >> atomize)
"present local premises as object-level statements" #>
- setup (Binding.name "rule") (Attrib.thms >> (fn ths => fn ctxt => some_rule ctxt ths))
+ setup @{binding rule} (Attrib.thms >> (fn ths => fn ctxt => some_rule ctxt ths))
"apply some intro/elim rule" #>
- setup (Binding.name "erule") (xrule_meth erule) "apply rule in elimination manner (improper)" #>
- setup (Binding.name "drule") (xrule_meth drule) "apply rule in destruct manner (improper)" #>
- setup (Binding.name "frule") (xrule_meth frule) "apply rule in forward manner (improper)" #>
- setup (Binding.name "this") (Scan.succeed (K this)) "apply current facts as rules" #>
- setup (Binding.name "fact") (Attrib.thms >> fact) "composition by facts from context" #>
- setup (Binding.name "assumption") (Scan.succeed assumption)
+ setup @{binding erule} (xrule_meth erule) "apply rule in elimination manner (improper)" #>
+ setup @{binding drule} (xrule_meth drule) "apply rule in destruct manner (improper)" #>
+ setup @{binding frule} (xrule_meth frule) "apply rule in forward manner (improper)" #>
+ setup @{binding this} (Scan.succeed (K this)) "apply current facts as rules" #>
+ setup @{binding fact} (Attrib.thms >> fact) "composition by facts from context" #>
+ setup @{binding assumption} (Scan.succeed assumption)
"proof by assumption, preferring facts" #>
- setup (Binding.name "rename_tac") (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name) >>
+ setup @{binding rename_tac} (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name) >>
(fn (quant, xs) => K (SIMPLE_METHOD'' quant (rename_tac xs))))
"rename parameters of goal" #>
- setup (Binding.name "rotate_tac") (Args.goal_spec -- Scan.lift (Scan.optional Parse.int 1) >>
+ setup @{binding rotate_tac} (Args.goal_spec -- Scan.lift (Scan.optional Parse.int 1) >>
(fn (quant, i) => K (SIMPLE_METHOD'' quant (rotate_tac i))))
"rotate assumptions of goal" #>
- setup (Binding.name "tactic") (Scan.lift Args.name_source_position >> tactic)
+ setup @{binding 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)
+ setup @{binding raw_tactic} (Scan.lift Args.name_source_position >> raw_tactic)
"ML tactic as raw proof method");
--- a/src/Pure/Thy/term_style.ML Tue Mar 18 13:36:28 2014 +0100
+++ b/src/Pure/Thy/term_style.ML Tue Mar 18 15:29:58 2014 +0100
@@ -84,10 +84,10 @@
| sub_term t = t;
val _ = Theory.setup
- (setup (Binding.name "lhs") (style_lhs_rhs fst) #>
- setup (Binding.name "rhs") (style_lhs_rhs snd) #>
- setup (Binding.name "prem") style_prem #>
- setup (Binding.name "concl") (Scan.succeed (K Logic.strip_imp_concl)) #>
- setup (Binding.name "sub") (Scan.succeed (K sub_term)));
+ (setup @{binding lhs} (style_lhs_rhs fst) #>
+ setup @{binding rhs} (style_lhs_rhs snd) #>
+ setup @{binding prem} style_prem #>
+ setup @{binding concl} (Scan.succeed (K Logic.strip_imp_concl)) #>
+ setup @{binding sub} (Scan.succeed (K sub_term)));
end;
--- a/src/Pure/Thy/thy_load.ML Tue Mar 18 13:36:28 2014 +0100
+++ b/src/Pure/Thy/thy_load.ML Tue Mar 18 15:29:58 2014 +0100
@@ -229,11 +229,11 @@
in
val _ = Theory.setup
- (Thy_Output.antiquotation (Binding.name "file") (Scan.lift (Parse.position Parse.path))
+ (Thy_Output.antiquotation @{binding file} (Scan.lift (Parse.position Parse.path))
(file_antiq true o #context) #>
- Thy_Output.antiquotation (Binding.name "file_unchecked") (Scan.lift (Parse.position Parse.path))
+ Thy_Output.antiquotation @{binding file_unchecked} (Scan.lift (Parse.position Parse.path))
(file_antiq false o #context) #>
- ML_Antiquotation.value (Binding.name "path")
+ ML_Antiquotation.value @{binding path}
(Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, arg) =>
let val path = check_path true ctxt Path.current arg
in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end)));
--- a/src/Pure/Thy/thy_output.ML Tue Mar 18 13:36:28 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML Tue Mar 18 15:29:58 2014 +0100
@@ -437,23 +437,23 @@
(* options *)
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));
+ (add_option @{binding show_types} (Config.put show_types o boolean) #>
+ add_option @{binding show_sorts} (Config.put show_sorts o boolean) #>
+ add_option @{binding show_structs} (Config.put show_structs o boolean) #>
+ add_option @{binding show_question_marks} (Config.put show_question_marks o boolean) #>
+ add_option @{binding show_abbrevs} (Config.put show_abbrevs o boolean) #>
+ add_option @{binding names_long} (Config.put Name_Space.names_long o boolean) #>
+ add_option @{binding names_short} (Config.put Name_Space.names_short o boolean) #>
+ add_option @{binding names_unique} (Config.put Name_Space.names_unique o boolean) #>
+ add_option @{binding eta_contract} (Config.put Syntax_Trans.eta_contract o boolean) #>
+ add_option @{binding display} (Config.put display o boolean) #>
+ add_option @{binding break} (Config.put break o boolean) #>
+ add_option @{binding quotes} (Config.put quotes o boolean) #>
+ add_option @{binding mode} (add_wrapper o Print_Mode.with_modes o single) #>
+ add_option @{binding margin} (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer) #>
+ add_option @{binding indent} (Config.put indent o integer) #>
+ add_option @{binding source} (Config.put source o boolean) #>
+ add_option @{binding goals_limit} (Config.put Goal_Display.goals_limit o integer));
(* basic pretty printing *)
@@ -565,20 +565,20 @@
in
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 = true, strict = false}) pretty_const #>
- basic_entity (Binding.name "abbrev") (Scan.lift Args.name_inner_syntax) pretty_abbrev #>
- basic_entity (Binding.name "typ") Args.typ_abbrev Syntax.pretty_typ #>
- basic_entity (Binding.name "class") (Scan.lift Args.name_inner_syntax) pretty_class #>
- basic_entity (Binding.name "type") (Scan.lift Args.name) pretty_type #>
- basic_entity (Binding.name "text") (Scan.lift Args.name_source_position) pretty_text_report #>
- 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);
+ (basic_entities_style @{binding thm} (Term_Style.parse -- Attrib.thms) pretty_thm_style #>
+ basic_entity @{binding prop} (Term_Style.parse -- Args.prop) pretty_term_style #>
+ basic_entity @{binding term} (Term_Style.parse -- Args.term) pretty_term_style #>
+ basic_entity @{binding term_type} (Term_Style.parse -- Args.term) pretty_term_typ #>
+ basic_entity @{binding typeof} (Term_Style.parse -- Args.term) pretty_term_typeof #>
+ basic_entity @{binding const} (Args.const {proper = true, strict = false}) pretty_const #>
+ basic_entity @{binding abbrev} (Scan.lift Args.name_inner_syntax) pretty_abbrev #>
+ basic_entity @{binding typ} Args.typ_abbrev Syntax.pretty_typ #>
+ basic_entity @{binding class} (Scan.lift Args.name_inner_syntax) pretty_class #>
+ basic_entity @{binding type} (Scan.lift Args.name) pretty_type #>
+ basic_entity @{binding text} (Scan.lift Args.name_source_position) pretty_text_report #>
+ basic_entities @{binding prf} Attrib.thms (pretty_prf false) #>
+ basic_entities @{binding full_prf} Attrib.thms (pretty_prf true) #>
+ basic_entity @{binding theory} (Scan.lift (Parse.position Args.name)) pretty_theory);
end;
@@ -600,8 +600,8 @@
in
val _ = Theory.setup
- (goal_state (Binding.name "goals") true #>
- goal_state (Binding.name "subgoals") false);
+ (goal_state @{binding goals} true #>
+ goal_state @{binding subgoals} false);
end;
@@ -611,7 +611,7 @@
val _ = Keyword.define ("by", NONE); (*overlap with command category*)
val _ = Theory.setup
- (antiquotation (Binding.name "lemma")
+ (antiquotation @{binding lemma}
(Scan.lift (Scan.ahead Parse.not_eof) -- Args.prop --
Scan.lift (Parse.position (Args.$$$ "by") -- Method.parse -- Scan.option Method.parse))
(fn {source, context = ctxt, ...} => fn ((prop_token, prop), (((_, by_pos), m1), m2)) =>
@@ -654,18 +654,18 @@
in
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_structure")
+ (ml_text @{binding ML} (ml_enclose "fn _ => (" ");") #>
+ ml_text @{binding ML_op} (ml_enclose "fn _ => (op " ");") #>
+ ml_text @{binding ML_type} (ml_enclose "val _ = NONE : (" ") option;") #>
+ ml_text @{binding ML_structure}
(ml_enclose "functor XXX() = struct structure XX = " " end;") #>
- ml_text (Binding.name "ML_functor") (* FIXME formal treatment of functor name (!?) *)
+ ml_text @{binding ML_functor} (* FIXME formal treatment of functor name (!?) *)
(fn source =>
ML_Lex.read Position.none ("ML_Env.check_functor " ^
ML_Syntax.print_string (#1 (Symbol_Pos.source_content source)))) #>
- ml_text (Binding.name "ML_text") (K []));
+ ml_text @{binding ML_text} (K []));
end;
@@ -673,7 +673,7 @@
(* URLs *)
val _ = Theory.setup
- (antiquotation (Binding.name "url") (Scan.lift (Parse.position Parse.name))
+ (antiquotation @{binding url} (Scan.lift (Parse.position Parse.name))
(fn {context = ctxt, ...} => fn (name, pos) =>
(Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url name)];
enclose "\\url{" "}" name)));
--- a/src/Pure/pure_syn.ML Tue Mar 18 13:36:28 2014 +0100
+++ b/src/Pure/pure_syn.ML Tue Mar 18 15:29:58 2014 +0100
@@ -9,8 +9,7 @@
val _ =
Outer_Syntax.command
- (("theory", Keyword.tag_theory Keyword.thy_begin), Position.file "pure_syn.ML")
- "begin theory context"
+ (("theory", Keyword.tag_theory Keyword.thy_begin), @{here}) "begin theory"
(Thy_Header.args >> (fn header =>
Toplevel.print o
Toplevel.init_theory
@@ -18,8 +17,7 @@
val _ =
Outer_Syntax.command
- (("ML_file", Keyword.tag_ml Keyword.thy_load), Position.file "pure_syn.ML")
- "ML text from file"
+ (("ML_file", Keyword.tag_ml Keyword.thy_load), @{here}) "ML text from file"
(Thy_Load.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy =>
let
val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy);
--- a/src/Pure/simplifier.ML Tue Mar 18 13:36:28 2014 +0100
+++ b/src/Pure/simplifier.ML Tue Mar 18 15:29:58 2014 +0100
@@ -144,7 +144,7 @@
val the_simproc = Name_Space.get o get_simprocs;
val _ = Theory.setup
- (ML_Antiquotation.value (Binding.name "simproc")
+ (ML_Antiquotation.value @{binding 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))));
@@ -315,13 +315,13 @@
(* setup attributes *)
val _ = Theory.setup
- (Attrib.setup (Binding.name simpN) (Attrib.add_del simp_add simp_del)
+ (Attrib.setup @{binding simp} (Attrib.add_del simp_add simp_del)
"declaration of Simplifier rewrite rule" #>
- Attrib.setup (Binding.name congN) (Attrib.add_del cong_add cong_del)
+ Attrib.setup @{binding cong} (Attrib.add_del cong_add cong_del)
"declaration of Simplifier congruence rule" #>
- Attrib.setup (Binding.name "simproc") simproc_att
+ Attrib.setup @{binding simproc} simproc_att
"declaration of simplification procedures" #>
- Attrib.setup (Binding.name "simplified") simplified "simplified rule");
+ Attrib.setup @{binding simplified} simplified "simplified rule");
@@ -362,12 +362,12 @@
(** setup **)
fun method_setup more_mods =
- Method.setup (Binding.name simpN)
+ Method.setup @{binding simp}
(simp_method more_mods (fn ctxt => fn tac => fn facts =>
HEADGOAL (Method.insert_tac facts THEN'
(CHANGED_PROP oo tac) ctxt)))
"simplification" #>
- Method.setup (Binding.name "simp_all")
+ Method.setup @{binding simp_all}
(simp_method more_mods (fn ctxt => fn tac => fn facts =>
ALLGOALS (Method.insert_tac facts) THEN
(CHANGED_PROP o PARALLEL_GOALS o ALLGOALS o tac) ctxt))