--- a/etc/symbols Mon Dec 12 17:40:06 2016 +0100
+++ b/etc/symbols Tue Dec 13 11:51:42 2016 +0100
@@ -361,7 +361,7 @@
\<comment> code: 0x002015 group: document font: IsabelleText
\<open> code: 0x002039 group: punctuation font: IsabelleText abbrev: <<
\<close> code: 0x00203a group: punctuation font: IsabelleText abbrev: >>
-\<here> code: 0x002302 font: IsabelleText
+\<^here> code: 0x002302 font: IsabelleText
\<^undefined> code: 0x002756 font: IsabelleText
\<^noindent> code: 0x0021e4 group: document font: IsabelleText
\<^smallskip> code: 0x002508 group: document font: IsabelleText
--- a/lib/texinputs/isabellesym.sty Mon Dec 12 17:40:06 2016 +0100
+++ b/lib/texinputs/isabellesym.sty Tue Dec 13 11:51:42 2016 +0100
@@ -370,3 +370,4 @@
\newcommand{\isactrlundefined}{\isakeyword{undefined}\ }
\newcommand{\isactrlfile}{\isakeyword{file}\ }
\newcommand{\isactrldir}{\isakeyword{dir}\ }
+\newcommand{\isactrlhere}{\isakeyword{here}\ }
--- a/src/HOL/Library/old_recdef.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/HOL/Library/old_recdef.ML Tue Dec 13 11:51:42 2016 +0100
@@ -2779,15 +2779,15 @@
val recdef_wfN = "recdef_wf";
val recdef_modifiers =
- [Args.$$$ recdef_simpN -- Args.colon >> K (Method.modifier simp_add @{here}),
- Args.$$$ recdef_simpN -- Args.add -- Args.colon >> K (Method.modifier simp_add @{here}),
- Args.$$$ recdef_simpN -- Args.del -- Args.colon >> K (Method.modifier simp_del @{here}),
- Args.$$$ recdef_congN -- Args.colon >> K (Method.modifier cong_add @{here}),
- Args.$$$ recdef_congN -- Args.add -- Args.colon >> K (Method.modifier cong_add @{here}),
- Args.$$$ recdef_congN -- Args.del -- Args.colon >> K (Method.modifier cong_del @{here}),
- Args.$$$ recdef_wfN -- Args.colon >> K (Method.modifier wf_add @{here}),
- Args.$$$ recdef_wfN -- Args.add -- Args.colon >> K (Method.modifier wf_add @{here}),
- Args.$$$ recdef_wfN -- Args.del -- Args.colon >> K (Method.modifier wf_del @{here})] @
+ [Args.$$$ recdef_simpN -- Args.colon >> K (Method.modifier simp_add \<^here>),
+ Args.$$$ recdef_simpN -- Args.add -- Args.colon >> K (Method.modifier simp_add \<^here>),
+ Args.$$$ recdef_simpN -- Args.del -- Args.colon >> K (Method.modifier simp_del \<^here>),
+ Args.$$$ recdef_congN -- Args.colon >> K (Method.modifier cong_add \<^here>),
+ Args.$$$ recdef_congN -- Args.add -- Args.colon >> K (Method.modifier cong_add \<^here>),
+ Args.$$$ recdef_congN -- Args.del -- Args.colon >> K (Method.modifier cong_del \<^here>),
+ Args.$$$ recdef_wfN -- Args.colon >> K (Method.modifier wf_add \<^here>),
+ Args.$$$ recdef_wfN -- Args.add -- Args.colon >> K (Method.modifier wf_add \<^here>),
+ Args.$$$ recdef_wfN -- Args.del -- Args.colon >> K (Method.modifier wf_del \<^here>)] @
Clasimp.clasimp_modifiers;
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Tue Dec 13 11:51:42 2016 +0100
@@ -315,7 +315,7 @@
THEN (DETERM (TRY (etac @{thm Pair_inject} 1)))*)
THEN (REPEAT_DETERM_N (num_of_constrs - 1)
(eresolve_tac ctxt @{thms botE} 1 ORELSE eresolve_tac ctxt @{thms botE} 2)))
- THEN assert_tac ctxt @{here} (fn st => Thm.nprems_of st <= 2)
+ THEN assert_tac ctxt \<^here> (fn st => Thm.nprems_of st <= 2)
THEN (EVERY (map split_term_tac ts))
end
else all_tac
--- a/src/Provers/clasimp.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Provers/clasimp.ML Tue Dec 13 11:51:42 2016 +0100
@@ -193,9 +193,9 @@
val iffN = "iff";
val iff_modifiers =
- [Args.$$$ iffN -- Scan.option Args.add -- Args.colon >> K (Method.modifier iff_add @{here}),
- Args.$$$ iffN -- Scan.option Args.add -- Args.query_colon >> K (Method.modifier iff_add' @{here}),
- Args.$$$ iffN -- Args.del -- Args.colon >> K (Method.modifier iff_del @{here})];
+ [Args.$$$ iffN -- Scan.option Args.add -- Args.colon >> K (Method.modifier iff_add \<^here>),
+ Args.$$$ iffN -- Scan.option Args.add -- Args.query_colon >> K (Method.modifier iff_add' \<^here>),
+ Args.$$$ iffN -- Args.del -- Args.colon >> K (Method.modifier iff_del \<^here>)];
val clasimp_modifiers =
Simplifier.simp_modifiers @ Splitter.split_modifiers @
--- a/src/Provers/classical.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Provers/classical.ML Tue Dec 13 11:51:42 2016 +0100
@@ -947,13 +947,13 @@
(* automatic methods *)
val cla_modifiers =
- [Args.$$$ destN -- Args.bang_colon >> K (Method.modifier (safe_dest NONE) @{here}),
- Args.$$$ destN -- Args.colon >> K (Method.modifier (unsafe_dest NONE) @{here}),
- Args.$$$ elimN -- Args.bang_colon >> K (Method.modifier (safe_elim NONE) @{here}),
- Args.$$$ elimN -- Args.colon >> K (Method.modifier (unsafe_elim NONE) @{here}),
- Args.$$$ introN -- Args.bang_colon >> K (Method.modifier (safe_intro NONE) @{here}),
- Args.$$$ introN -- Args.colon >> K (Method.modifier (unsafe_intro NONE) @{here}),
- Args.del -- Args.colon >> K (Method.modifier rule_del @{here})];
+ [Args.$$$ destN -- Args.bang_colon >> K (Method.modifier (safe_dest NONE) \<^here>),
+ Args.$$$ destN -- Args.colon >> K (Method.modifier (unsafe_dest NONE) \<^here>),
+ Args.$$$ elimN -- Args.bang_colon >> K (Method.modifier (safe_elim NONE) \<^here>),
+ Args.$$$ elimN -- Args.colon >> K (Method.modifier (unsafe_elim NONE) \<^here>),
+ Args.$$$ introN -- Args.bang_colon >> K (Method.modifier (safe_intro NONE) \<^here>),
+ Args.$$$ introN -- Args.colon >> K (Method.modifier (unsafe_intro NONE) \<^here>),
+ Args.del -- Args.colon >> K (Method.modifier rule_del \<^here>)];
fun cla_method tac = Method.sections cla_modifiers >> K (SIMPLE_METHOD o tac);
fun cla_method' tac = Method.sections cla_modifiers >> K (SIMPLE_METHOD' o tac);
--- a/src/Provers/splitter.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Provers/splitter.ML Tue Dec 13 11:51:42 2016 +0100
@@ -473,9 +473,9 @@
(* methods *)
val split_modifiers =
- [Args.$$$ splitN -- Args.colon >> K (Method.modifier (split_add false) @{here}),
- Args.$$$ splitN -- Args.bang_colon >> K (Method.modifier (split_add true) @{here}),
- Args.$$$ splitN -- Args.del -- Args.colon >> K (Method.modifier split_del @{here})];
+ [Args.$$$ splitN -- Args.colon >> K (Method.modifier (split_add false) \<^here>),
+ Args.$$$ splitN -- Args.bang_colon >> K (Method.modifier (split_add true) \<^here>),
+ Args.$$$ splitN -- Args.del -- Args.colon >> K (Method.modifier split_del \<^here>)];
val _ =
Theory.setup
--- a/src/Pure/General/name_space.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/General/name_space.ML Tue Dec 13 11:51:42 2016 +0100
@@ -213,13 +213,13 @@
(* extern *)
-val names_long_raw = Config.declare_option ("names_long", @{here});
+val names_long_raw = Config.declare_option ("names_long", \<^here>);
val names_long = Config.bool names_long_raw;
-val names_short_raw = Config.declare_option ("names_short", @{here});
+val names_short_raw = Config.declare_option ("names_short", \<^here>);
val names_short = Config.bool names_short_raw;
-val names_unique_raw = Config.declare_option ("names_unique", @{here});
+val names_unique_raw = Config.declare_option ("names_unique", \<^here>);
val names_unique = Config.bool names_unique_raw;
fun extern ctxt space name =
--- a/src/Pure/General/position.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/General/position.ML Tue Dec 13 11:51:42 2016 +0100
@@ -208,7 +208,7 @@
(SOME i, NONE) => (" ", "(line " ^ Value.print_int i ^ ")")
| (SOME i, SOME name) => (" ", "(line " ^ Value.print_int i ^ " of " ^ quote name ^ ")")
| (NONE, SOME name) => (" ", "(file " ^ quote name ^ ")")
- | _ => if is_reported pos then ("", "\<here>") else ("", ""));
+ | _ => if is_reported pos then ("", "\092<^here>") else ("", ""));
in
if null props then ""
else s1 ^ Markup.markup (Markup.properties props Markup.position) s2
--- a/src/Pure/Isar/attrib.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/Isar/attrib.ML Tue Dec 13 11:51:42 2016 +0100
@@ -216,7 +216,7 @@
(* internal attribute *)
val _ = Theory.setup
- (setup (Binding.make ("attribute", @{here}))
+ (setup (Binding.make ("attribute", \<^here>))
(Scan.lift Args.internal_attribute >> Morphism.form)
"internal attribute");
--- a/src/Pure/Isar/local_defs.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/Isar/local_defs.ML Tue Dec 13 11:51:42 2016 +0100
@@ -207,7 +207,7 @@
(* unfold object-level rules *)
-val unfold_abs_def_raw = Config.declare ("unfold_abs_def", @{here}) (K (Config.Bool true));
+val unfold_abs_def_raw = Config.declare ("unfold_abs_def", \<^here>) (K (Config.Bool true));
val unfold_abs_def = Config.bool unfold_abs_def_raw;
local
--- a/src/Pure/Isar/method.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/Isar/method.ML Tue Dec 13 11:51:42 2016 +0100
@@ -393,7 +393,7 @@
val _ =
Theory.setup
- (Global_Theory.add_thms_dynamic (Binding.make ("method_facts", @{here}), get_facts_generic));
+ (Global_Theory.add_thms_dynamic (Binding.make ("method_facts", \<^here>), get_facts_generic));
(* method text *)
@@ -497,7 +497,7 @@
val _ = Seq.pull (method ctxt' src' ctxt' [] (ctxt', Goal.protect 0 Drule.dummy_thm));
in map Token.closure src' end;
-val closure = Config.bool (Config.declare ("Method.closure", @{here}) (K (Config.Bool true)));
+val closure = Config.bool (Config.declare ("Method.closure", \<^here>) (K (Config.Bool true)));
fun method_cmd ctxt =
check_src ctxt #>
@@ -608,7 +608,7 @@
(* sections *)
val old_section_parser =
- Config.bool (Config.declare ("Method.old_section_parser", @{here}) (K (Config.Bool false)));
+ Config.bool (Config.declare ("Method.old_section_parser", \<^here>) (K (Config.Bool false)));
local
--- a/src/Pure/Isar/outer_syntax.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/Isar/outer_syntax.ML Tue Dec 13 11:51:42 2016 +0100
@@ -175,7 +175,7 @@
(* parse commands *)
val bootstrap =
- Config.bool (Config.declare ("Outer_Syntax.bootstrap", @{here}) (K (Config.Bool true)));
+ Config.bool (Config.declare ("Outer_Syntax.bootstrap", \<^here>) (K (Config.Bool true)));
local
@@ -322,7 +322,7 @@
(* 'ML' command -- required for bootstrapping Isar *)
val _ =
- command ("ML", @{here}) "ML text within theory or local theory"
+ command ("ML", \<^here>) "ML text within theory or local theory"
(Parse.ML_source >> (fn source =>
Toplevel.generic_theory
(ML_Context.exec (fn () =>
--- a/src/Pure/Isar/proof_context.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/Isar/proof_context.ML Tue Dec 13 11:51:42 2016 +0100
@@ -633,7 +633,7 @@
end;
-val show_abbrevs_raw = Config.declare ("show_abbrevs", @{here}) (fn _ => Config.Bool true);
+val show_abbrevs_raw = Config.declare ("show_abbrevs", \<^here>) (fn _ => Config.Bool true);
val show_abbrevs = Config.bool show_abbrevs_raw;
fun contract_abbrevs ctxt t =
@@ -667,7 +667,7 @@
local
val dummies =
- Config.bool (Config.declare ("Proof_Context.dummies", @{here}) (K (Config.Bool false)));
+ Config.bool (Config.declare ("Proof_Context.dummies", \<^here>) (K (Config.Bool false)));
fun check_dummies ctxt t =
if Config.get ctxt dummies then t
@@ -979,7 +979,7 @@
(* retrieve facts *)
val dynamic_facts_dummy =
- Config.bool (Config.declare ("dynamic_facts_dummy_", @{here}) (fn _ => Config.Bool false));
+ Config.bool (Config.declare ("dynamic_facts_dummy_", \<^here>) (fn _ => Config.Bool false));
local
@@ -1049,7 +1049,7 @@
(* inner statement mode *)
val inner_stmt =
- Config.bool (Config.declare ("inner_stmt", @{here}) (K (Config.Bool false)));
+ Config.bool (Config.declare ("inner_stmt", \<^here>) (K (Config.Bool false)));
fun is_stmt ctxt = Config.get ctxt inner_stmt;
val set_stmt = Config.put inner_stmt;
@@ -1571,10 +1571,10 @@
(* core context *)
val debug =
- Config.bool (Config.declare ("Proof_Context.debug", @{here}) (K (Config.Bool false)));
+ Config.bool (Config.declare ("Proof_Context.debug", \<^here>) (K (Config.Bool false)));
val verbose =
- Config.bool (Config.declare ("Proof_Context.verbose", @{here}) (K (Config.Bool false)));
+ Config.bool (Config.declare ("Proof_Context.verbose", \<^here>) (K (Config.Bool false)));
fun pretty_ctxt ctxt =
if not (Config.get ctxt debug) then []
--- a/src/Pure/ML/ml_antiquotation.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/ML/ml_antiquotation.ML Tue Dec 13 11:51:42 2016 +0100
@@ -34,16 +34,16 @@
(* basic antiquotations *)
val _ = Theory.setup
- (declaration (Binding.make ("here", @{here})) (Scan.succeed ())
+ (declaration (Binding.make ("here", \<^here>)) (Scan.succeed ())
(fn src => fn () =>
ML_Context.value_decl "position" (ML_Syntax.print_position (#2 (Token.name_of_src src)))) #>
- inline (Binding.make ("make_string", @{here})) (Args.context >> K ML_Pretty.make_string_fn) #>
+ inline (Binding.make ("make_string", \<^here>)) (Args.context >> K ML_Pretty.make_string_fn) #>
- value (Binding.make ("binding", @{here}))
+ value (Binding.make ("binding", \<^here>))
(Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding) #>
- value (Binding.make ("cartouche", @{here}))
+ value (Binding.make ("cartouche", \<^here>))
(Scan.lift Args.cartouche_input >> (fn source =>
"Input.source true " ^ ML_Syntax.print_string (Input.text_of source) ^ " " ^
ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source)))));
--- a/src/Pure/ML/ml_compiler0.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/ML/ml_compiler0.ML Tue Dec 13 11:51:42 2016 +0100
@@ -63,7 +63,7 @@
fun ml_input start_line name txt =
let
- fun input line (#"@" :: #"{" :: #"h" :: #"e" :: #"r" :: #"e" :: #"}" :: cs) res =
+ fun input line (#"\\" :: #"<" :: #"^" :: #"h" :: #"e" :: #"r" :: #"e" :: #">" :: cs) res =
let val s = "(Position.line_file_only " ^ Int.toString line ^ " \"" ^ name ^ "\")"
in input line cs (s :: res) end
| input line (#"@" :: #"{" :: #"m" :: #"a" :: #"k" :: #"e" :: #"_" ::
--- a/src/Pure/ML/ml_env.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/ML/ml_env.ML Tue Dec 13 11:51:42 2016 +0100
@@ -98,7 +98,7 @@
(* SML environment for Isabelle/ML *)
val SML_environment =
- Config.bool (Config.declare ("SML_environment", @{here}) (fn _ => Config.Bool false));
+ Config.bool (Config.declare ("SML_environment", \<^here>) (fn _ => Config.Bool false));
fun sml_env SML =
SML orelse
--- a/src/Pure/ML/ml_options.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/ML/ml_options.ML Tue Dec 13 11:51:42 2016 +0100
@@ -25,13 +25,13 @@
(* source trace *)
val source_trace_raw =
- Config.declare ("ML_source_trace", @{here}) (fn _ => Config.Bool false);
+ Config.declare ("ML_source_trace", \<^here>) (fn _ => Config.Bool false);
val source_trace = Config.bool source_trace_raw;
(* exception trace *)
-val exception_trace_raw = Config.declare_option ("ML_exception_trace", @{here});
+val exception_trace_raw = Config.declare_option ("ML_exception_trace", \<^here>);
val exception_trace = Config.bool exception_trace_raw;
fun exception_trace_enabled NONE =
@@ -41,7 +41,7 @@
(* exception debugger *)
-val exception_debugger_raw = Config.declare_option ("ML_exception_debugger", @{here});
+val exception_debugger_raw = Config.declare_option ("ML_exception_debugger", \<^here>);
val exception_debugger = Config.bool exception_debugger_raw;
fun exception_debugger_enabled NONE =
@@ -51,7 +51,7 @@
(* debugger *)
-val debugger_raw = Config.declare_option ("ML_debugger", @{here});
+val debugger_raw = Config.declare_option ("ML_debugger", \<^here>);
val debugger = Config.bool debugger_raw;
fun debugger_enabled NONE =
--- a/src/Pure/ML/ml_print_depth.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/ML/ml_print_depth.ML Tue Dec 13 11:51:42 2016 +0100
@@ -18,7 +18,7 @@
val set_print_depth = ML_Print_Depth.set_print_depth;
val print_depth_raw =
- Config.declare ("ML_print_depth", @{here})
+ Config.declare ("ML_print_depth", \<^here>)
(fn _ => Config.Int (ML_Print_Depth.get_print_depth ()));
val print_depth = Config.int print_depth_raw;
--- a/src/Pure/Proof/extraction.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/Proof/extraction.ML Tue Dec 13 11:51:42 2016 +0100
@@ -37,13 +37,13 @@
val add_syntax =
Sign.root_path
#> Sign.add_types_global
- [(Binding.make ("Type", @{here}), 0, NoSyn),
- (Binding.make ("Null", @{here}), 0, NoSyn)]
+ [(Binding.make ("Type", \<^here>), 0, NoSyn),
+ (Binding.make ("Null", \<^here>), 0, NoSyn)]
#> Sign.add_consts
- [(Binding.make ("typeof", @{here}), typ "'b => Type", NoSyn),
- (Binding.make ("Type", @{here}), typ "'a itself => Type", NoSyn),
- (Binding.make ("Null", @{here}), typ "Null", NoSyn),
- (Binding.make ("realizes", @{here}), typ "'a => 'b => 'b", NoSyn)];
+ [(Binding.make ("typeof", \<^here>), typ "'b => Type", NoSyn),
+ (Binding.make ("Type", \<^here>), typ "'a itself => Type", NoSyn),
+ (Binding.make ("Null", \<^here>), typ "Null", NoSyn),
+ (Binding.make ("realizes", \<^here>), typ "'a => 'b => 'b", NoSyn)];
val nullT = Type ("Null", []);
val nullt = Const ("Null", nullT);
--- a/src/Pure/Proof/proof_syntax.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/Proof/proof_syntax.ML Tue Dec 13 11:51:42 2016 +0100
@@ -48,19 +48,19 @@
|> Sign.root_path
|> Sign.set_defsort []
|> Sign.add_types_global
- [(Binding.make ("proof", @{here}), 0, NoSyn)]
+ [(Binding.make ("proof", \<^here>), 0, NoSyn)]
|> fold (snd oo Sign.declare_const_global)
- [((Binding.make ("Appt", @{here}), [proofT, aT] ---> proofT), mixfix ("(1_ \<cdot>/ _)", [4, 5], 4)),
- ((Binding.make ("AppP", @{here}), [proofT, proofT] ---> proofT), mixfix ("(1_ \<bullet>/ _)", [4, 5], 4)),
- ((Binding.make ("Abst", @{here}), (aT --> proofT) --> proofT), NoSyn),
- ((Binding.make ("AbsP", @{here}), [propT, proofT --> proofT] ---> proofT), NoSyn),
- ((Binding.make ("Hyp", @{here}), propT --> proofT), NoSyn),
- ((Binding.make ("Oracle", @{here}), propT --> proofT), NoSyn),
- ((Binding.make ("OfClass", @{here}), (Term.a_itselfT --> propT) --> proofT), NoSyn),
- ((Binding.make ("MinProof", @{here}), proofT), Mixfix.mixfix "?")]
+ [((Binding.make ("Appt", \<^here>), [proofT, aT] ---> proofT), mixfix ("(1_ \<cdot>/ _)", [4, 5], 4)),
+ ((Binding.make ("AppP", \<^here>), [proofT, proofT] ---> proofT), mixfix ("(1_ \<bullet>/ _)", [4, 5], 4)),
+ ((Binding.make ("Abst", \<^here>), (aT --> proofT) --> proofT), NoSyn),
+ ((Binding.make ("AbsP", \<^here>), [propT, proofT --> proofT] ---> proofT), NoSyn),
+ ((Binding.make ("Hyp", \<^here>), propT --> proofT), NoSyn),
+ ((Binding.make ("Oracle", \<^here>), propT --> proofT), NoSyn),
+ ((Binding.make ("OfClass", \<^here>), (Term.a_itselfT --> propT) --> proofT), NoSyn),
+ ((Binding.make ("MinProof", \<^here>), proofT), Mixfix.mixfix "?")]
|> Sign.add_nonterminals_global
- [Binding.make ("param", @{here}),
- Binding.make ("params", @{here})]
+ [Binding.make ("param", \<^here>),
+ Binding.make ("params", \<^here>)]
|> Sign.add_syntax Syntax.mode_default
[("_Lam", [paramsT, proofT] ---> proofT, mixfix ("(1\<^bold>\<lambda>_./ _)", [0, 3], 3)),
("_Lam0", [paramT, paramsT] ---> paramsT, mixfix ("_/ _", [1, 0], 0)),
--- a/src/Pure/Proof/reconstruct.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/Proof/reconstruct.ML Tue Dec 13 11:51:42 2016 +0100
@@ -19,7 +19,7 @@
struct
val quiet_mode =
- Config.bool (Config.declare ("Reconstruct.quiet_mode", @{here}) (K (Config.Bool true)));
+ Config.bool (Config.declare ("Reconstruct.quiet_mode", \<^here>) (K (Config.Bool true)));
fun message ctxt msg =
if Config.get ctxt quiet_mode then () else writeln (msg ());
--- a/src/Pure/Syntax/ast.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/Syntax/ast.ML Tue Dec 13 11:51:42 2016 +0100
@@ -166,10 +166,10 @@
(* normalize *)
-val trace_raw = Config.declare ("syntax_ast_trace", @{here}) (fn _ => Config.Bool false);
+val trace_raw = Config.declare ("syntax_ast_trace", \<^here>) (fn _ => Config.Bool false);
val trace = Config.bool trace_raw;
-val stats_raw = Config.declare ("syntax_ast_stats", @{here}) (fn _ => Config.Bool false);
+val stats_raw = Config.declare ("syntax_ast_stats", \<^here>) (fn _ => Config.Bool false);
val stats = Config.bool stats_raw;
fun message head body =
--- a/src/Pure/Syntax/parser.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/Syntax/parser.ML Tue Dec 13 11:51:42 2016 +0100
@@ -627,7 +627,7 @@
(*trigger value for warnings*)
val branching_level =
- Config.int (Config.declare ("syntax_branching_level", @{here}) (fn _ => Config.Int 600));
+ Config.int (Config.declare ("syntax_branching_level", \<^here>) (fn _ => Config.Int 600));
(*get all productions of a NT and NTs chained to it which can
be started by specified token*)
--- a/src/Pure/Syntax/printer.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/Syntax/printer.ML Tue Dec 13 11:51:42 2016 +0100
@@ -48,29 +48,29 @@
(** options for printing **)
-val show_brackets_raw = Config.declare_option ("show_brackets", @{here});
+val show_brackets_raw = Config.declare_option ("show_brackets", \<^here>);
val show_brackets = Config.bool show_brackets_raw;
-val show_types_raw = Config.declare_option ("show_types", @{here});
+val show_types_raw = Config.declare_option ("show_types", \<^here>);
val show_types = Config.bool show_types_raw;
-val show_sorts_raw = Config.declare_option ("show_sorts", @{here});
+val show_sorts_raw = Config.declare_option ("show_sorts", \<^here>);
val show_sorts = Config.bool show_sorts_raw;
val show_markup_default = Unsynchronized.ref false;
val show_markup_raw =
- Config.declare ("show_markup", @{here}) (fn _ => Config.Bool (! show_markup_default));
+ Config.declare ("show_markup", \<^here>) (fn _ => Config.Bool (! show_markup_default));
val show_markup = Config.bool show_markup_raw;
val show_structs_raw =
- Config.declare ("show_structs", @{here}) (fn _ => Config.Bool false);
+ Config.declare ("show_structs", \<^here>) (fn _ => Config.Bool false);
val show_structs = Config.bool show_structs_raw;
-val show_question_marks_raw = Config.declare_option ("show_question_marks", @{here});
+val show_question_marks_raw = Config.declare_option ("show_question_marks", \<^here>);
val show_question_marks = Config.bool show_question_marks_raw;
val show_type_emphasis =
- Config.bool (Config.declare ("show_type_emphasis", @{here}) (fn _ => Config.Bool true));
+ Config.bool (Config.declare ("show_type_emphasis", \<^here>) (fn _ => Config.Bool true));
fun type_emphasis ctxt T =
T <> dummyT andalso
@@ -169,7 +169,7 @@
| is_chain _ = false;
val pretty_priority =
- Config.int (Config.declare ("Syntax.pretty_priority", @{here}) (K (Config.Int 0)));
+ Config.int (Config.declare ("Syntax.pretty_priority", \<^here>) (K (Config.Int 0)));
fun pretty type_mode curried ctxt tabs trf markup_trans markup_extern ast0 =
let
--- a/src/Pure/Syntax/syntax.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/Syntax/syntax.ML Tue Dec 13 11:51:42 2016 +0100
@@ -160,14 +160,14 @@
(* configuration options *)
-val root = Config.string (Config.declare ("syntax_root", @{here}) (K (Config.String "any")));
+val root = Config.string (Config.declare ("syntax_root", \<^here>) (K (Config.String "any")));
val ambiguity_warning_raw =
- Config.declare ("syntax_ambiguity_warning", @{here}) (fn _ => Config.Bool true);
+ Config.declare ("syntax_ambiguity_warning", \<^here>) (fn _ => Config.Bool true);
val ambiguity_warning = Config.bool ambiguity_warning_raw;
val ambiguity_limit_raw =
- Config.declare ("syntax_ambiguity_limit", @{here}) (fn _ => Config.Int 10);
+ Config.declare ("syntax_ambiguity_limit", \<^here>) (fn _ => Config.Int 10);
val ambiguity_limit = Config.int ambiguity_limit_raw;
@@ -330,7 +330,7 @@
(* global pretty printing *)
val pretty_global =
- Config.bool (Config.declare ("Syntax.pretty_global", @{here}) (K (Config.Bool false)));
+ Config.bool (Config.declare ("Syntax.pretty_global", \<^here>) (K (Config.Bool false)));
fun is_pretty_global ctxt = Config.get ctxt pretty_global;
val set_pretty_global = Config.put pretty_global;
val init_pretty_global = set_pretty_global true o Proof_Context.init_global;
--- a/src/Pure/Syntax/syntax_trans.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/Syntax/syntax_trans.ML Tue Dec 13 11:51:42 2016 +0100
@@ -297,7 +297,7 @@
| t' => Abs (a, T, t'))
| eta_abs t = t;
-val eta_contract_raw = Config.declare_option ("eta_contract", @{here});
+val eta_contract_raw = Config.declare_option ("eta_contract", \<^here>);
val eta_contract = Config.bool eta_contract_raw;
fun eta_contr ctxt tm =
--- a/src/Pure/Thy/thy_header.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/Thy/thy_header.ML Tue Dec 13 11:51:42 2016 +0100
@@ -64,28 +64,28 @@
val bootstrap_keywords =
Keyword.empty_keywords
|> Keyword.add_keywords
- [(("%", @{here}), Keyword.no_spec),
- (("(", @{here}), Keyword.no_spec),
- ((")", @{here}), Keyword.no_spec),
- ((",", @{here}), Keyword.no_spec),
- (("::", @{here}), Keyword.no_spec),
- (("=", @{here}), Keyword.no_spec),
- (("and", @{here}), Keyword.no_spec),
- ((beginN, @{here}), Keyword.quasi_command_spec),
- ((importsN, @{here}), Keyword.quasi_command_spec),
- ((keywordsN, @{here}), Keyword.quasi_command_spec),
- ((abbrevsN, @{here}), Keyword.quasi_command_spec),
- ((chapterN, @{here}), ((Keyword.document_heading, []), [])),
- ((sectionN, @{here}), ((Keyword.document_heading, []), [])),
- ((subsectionN, @{here}), ((Keyword.document_heading, []), [])),
- ((subsubsectionN, @{here}), ((Keyword.document_heading, []), [])),
- ((paragraphN, @{here}), ((Keyword.document_heading, []), [])),
- ((subparagraphN, @{here}), ((Keyword.document_heading, []), [])),
- ((textN, @{here}), ((Keyword.document_body, []), [])),
- ((txtN, @{here}), ((Keyword.document_body, []), [])),
- ((text_rawN, @{here}), ((Keyword.document_raw, []), [])),
- ((theoryN, @{here}), ((Keyword.thy_begin, []), ["theory"])),
- (("ML", @{here}), ((Keyword.thy_decl, []), ["ML"]))];
+ [(("%", \<^here>), Keyword.no_spec),
+ (("(", \<^here>), Keyword.no_spec),
+ ((")", \<^here>), Keyword.no_spec),
+ ((",", \<^here>), Keyword.no_spec),
+ (("::", \<^here>), Keyword.no_spec),
+ (("=", \<^here>), Keyword.no_spec),
+ (("and", \<^here>), Keyword.no_spec),
+ ((beginN, \<^here>), Keyword.quasi_command_spec),
+ ((importsN, \<^here>), Keyword.quasi_command_spec),
+ ((keywordsN, \<^here>), Keyword.quasi_command_spec),
+ ((abbrevsN, \<^here>), Keyword.quasi_command_spec),
+ ((chapterN, \<^here>), ((Keyword.document_heading, []), [])),
+ ((sectionN, \<^here>), ((Keyword.document_heading, []), [])),
+ ((subsectionN, \<^here>), ((Keyword.document_heading, []), [])),
+ ((subsubsectionN, \<^here>), ((Keyword.document_heading, []), [])),
+ ((paragraphN, \<^here>), ((Keyword.document_heading, []), [])),
+ ((subparagraphN, \<^here>), ((Keyword.document_heading, []), [])),
+ ((textN, \<^here>), ((Keyword.document_body, []), [])),
+ ((txtN, \<^here>), ((Keyword.document_body, []), [])),
+ ((text_rawN, \<^here>), ((Keyword.document_raw, []), [])),
+ ((theoryN, \<^here>), ((Keyword.thy_begin, []), ["theory"])),
+ (("ML", \<^here>), ((Keyword.thy_decl, []), ["ML"]))];
(* theory data *)
--- a/src/Pure/Thy/thy_output.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/Thy/thy_output.ML Tue Dec 13 11:51:42 2016 +0100
@@ -44,13 +44,13 @@
(** options **)
-val display = Attrib.setup_option_bool ("thy_output_display", @{here});
-val break = Attrib.setup_option_bool ("thy_output_break", @{here});
-val quotes = Attrib.setup_option_bool ("thy_output_quotes", @{here});
-val margin = Attrib.setup_option_int ("thy_output_margin", @{here});
-val indent = Attrib.setup_option_int ("thy_output_indent", @{here});
-val source = Attrib.setup_option_bool ("thy_output_source", @{here});
-val modes = Attrib.setup_option_string ("thy_output_modes", @{here});
+val display = Attrib.setup_option_bool ("thy_output_display", \<^here>);
+val break = Attrib.setup_option_bool ("thy_output_break", \<^here>);
+val quotes = Attrib.setup_option_bool ("thy_output_quotes", \<^here>);
+val margin = Attrib.setup_option_int ("thy_output_margin", \<^here>);
+val indent = Attrib.setup_option_int ("thy_output_indent", \<^here>);
+val source = Attrib.setup_option_bool ("thy_output_source", \<^here>);
+val modes = Attrib.setup_option_string ("thy_output_modes", \<^here>);
structure Wrappers = Proof_Data
--- a/src/Pure/Tools/find_consts.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/Tools/find_consts.ML Tue Dec 13 11:51:42 2016 +0100
@@ -141,7 +141,7 @@
Parse.typ >> Loose;
val query_keywords =
- Keyword.add_keywords [((":", @{here}), Keyword.no_spec)] Keyword.empty_keywords;
+ Keyword.add_keywords [((":", \<^here>), Keyword.no_spec)] Keyword.empty_keywords;
in
--- a/src/Pure/Tools/find_theorems.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/Tools/find_theorems.ML Tue Dec 13 11:51:42 2016 +0100
@@ -522,7 +522,7 @@
Parse.term >> Pattern;
val query_keywords =
- Keyword.add_keywords [((":", @{here}), Keyword.no_spec)] Keyword.empty_keywords;
+ Keyword.add_keywords [((":", \<^here>), Keyword.no_spec)] Keyword.empty_keywords;
in
--- a/src/Pure/conjunction.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/conjunction.ML Tue Dec 13 11:51:42 2016 +0100
@@ -85,13 +85,13 @@
in
val conjunctionD1 =
- Drule.store_standard_thm (Binding.make ("conjunctionD1", @{here})) (conjunctionD #1);
+ Drule.store_standard_thm (Binding.make ("conjunctionD1", \<^here>)) (conjunctionD #1);
val conjunctionD2 =
- Drule.store_standard_thm (Binding.make ("conjunctionD2", @{here})) (conjunctionD #2);
+ Drule.store_standard_thm (Binding.make ("conjunctionD2", \<^here>)) (conjunctionD #2);
val conjunctionI =
- Drule.store_standard_thm (Binding.make ("conjunctionI", @{here}))
+ Drule.store_standard_thm (Binding.make ("conjunctionI", \<^here>))
(Drule.implies_intr_list [A, B]
(Thm.equal_elim
(Thm.symmetric conjunction_def)
--- a/src/Pure/drule.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/drule.ML Tue Dec 13 11:51:42 2016 +0100
@@ -363,13 +363,13 @@
val reflexive_thm =
let val cx = certify (Var(("x",0),TVar(("'a",0),[])))
- in store_standard_thm_open (Binding.make ("reflexive", @{here})) (Thm.reflexive cx) end;
+ in store_standard_thm_open (Binding.make ("reflexive", \<^here>)) (Thm.reflexive cx) end;
val symmetric_thm =
let
val xy = read_prop "x::'a == y::'a";
val thm = Thm.implies_intr xy (Thm.symmetric (Thm.assume xy));
- in store_standard_thm_open (Binding.make ("symmetric", @{here})) thm end;
+ in store_standard_thm_open (Binding.make ("symmetric", \<^here>)) thm end;
val transitive_thm =
let
@@ -378,7 +378,7 @@
val xythm = Thm.assume xy;
val yzthm = Thm.assume yz;
val thm = Thm.implies_intr yz (Thm.transitive xythm yzthm);
- in store_standard_thm_open (Binding.make ("transitive", @{here})) thm end;
+ in store_standard_thm_open (Binding.make ("transitive", \<^here>)) thm end;
fun extensional eq =
let val eq' =
@@ -386,7 +386,7 @@
in Thm.equal_elim (Thm.eta_conversion (Thm.cprop_of eq')) eq' end;
val equals_cong =
- store_standard_thm_open (Binding.make ("equals_cong", @{here}))
+ store_standard_thm_open (Binding.make ("equals_cong", \<^here>))
(Thm.reflexive (read_prop "x::'a == y::'a"));
val imp_cong =
@@ -396,7 +396,7 @@
val AC = read_prop "A ==> C"
val A = read_prop "A"
in
- store_standard_thm_open (Binding.make ("imp_cong", @{here}))
+ store_standard_thm_open (Binding.make ("imp_cong", \<^here>))
(Thm.implies_intr ABC (Thm.equal_intr
(Thm.implies_intr AB (Thm.implies_intr A
(Thm.equal_elim (Thm.implies_elim (Thm.assume ABC) (Thm.assume A))
@@ -413,7 +413,7 @@
val A = read_prop "A"
val B = read_prop "B"
in
- store_standard_thm_open (Binding.make ("swap_prems_eq", @{here}))
+ store_standard_thm_open (Binding.make ("swap_prems_eq", \<^here>))
(Thm.equal_intr
(Thm.implies_intr ABC (Thm.implies_intr B (Thm.implies_intr A
(Thm.implies_elim (Thm.implies_elim (Thm.assume ABC) (Thm.assume A)) (Thm.assume B)))))
@@ -473,12 +473,12 @@
(*The rule V/V, obtains assumption solving for eresolve_tac*)
val asm_rl =
- store_standard_thm_open (Binding.make ("asm_rl", @{here}))
+ store_standard_thm_open (Binding.make ("asm_rl", \<^here>))
(Thm.trivial (read_prop "?psi"));
(*Meta-level cut rule: [| V==>W; V |] ==> W *)
val cut_rl =
- store_standard_thm_open (Binding.make ("cut_rl", @{here}))
+ store_standard_thm_open (Binding.make ("cut_rl", \<^here>))
(Thm.trivial (read_prop "?psi ==> ?theta"));
(*Generalized elim rule for one conclusion; cut_rl with reversed premises:
@@ -488,7 +488,7 @@
val V = read_prop "V";
val VW = read_prop "V ==> W";
in
- store_standard_thm_open (Binding.make ("revcut_rl", @{here}))
+ store_standard_thm_open (Binding.make ("revcut_rl", \<^here>))
(Thm.implies_intr V
(Thm.implies_intr VW (Thm.implies_elim (Thm.assume VW) (Thm.assume V))))
end;
@@ -499,7 +499,7 @@
val V = read_prop "V";
val W = read_prop "W";
val thm = Thm.implies_intr V (Thm.implies_intr W (Thm.assume W));
- in store_standard_thm_open (Binding.make ("thin_rl", @{here})) thm end;
+ in store_standard_thm_open (Binding.make ("thin_rl", \<^here>)) thm end;
(* (!!x. PROP ?V) == PROP ?V Allows removal of redundant parameters*)
val triv_forall_equality =
@@ -508,7 +508,7 @@
val QV = read_prop "!!x::'a. V";
val x = certify (Free ("x", Term.aT []));
in
- store_standard_thm_open (Binding.make ("triv_forall_equality", @{here}))
+ store_standard_thm_open (Binding.make ("triv_forall_equality", \<^here>))
(Thm.equal_intr (Thm.implies_intr QV (Thm.forall_elim x (Thm.assume QV)))
(Thm.implies_intr V (Thm.forall_intr x (Thm.assume V))))
end;
@@ -521,7 +521,7 @@
val AAB = read_prop "Phi ==> Phi ==> Psi";
val A = read_prop "Phi";
in
- store_standard_thm_open (Binding.make ("distinct_prems_rl", @{here}))
+ store_standard_thm_open (Binding.make ("distinct_prems_rl", \<^here>))
(implies_intr_list [AAB, A]
(implies_elim_list (Thm.assume AAB) [Thm.assume A, Thm.assume A]))
end;
@@ -535,7 +535,7 @@
val PQ = read_prop "phi ==> psi";
val QP = read_prop "psi ==> phi";
in
- store_standard_thm_open (Binding.make ("equal_intr_rule", @{here}))
+ store_standard_thm_open (Binding.make ("equal_intr_rule", \<^here>))
(Thm.implies_intr PQ
(Thm.implies_intr QP (Thm.equal_intr (Thm.assume PQ) (Thm.assume QP))))
end;
@@ -546,13 +546,13 @@
val eq = read_prop "phi::prop == psi::prop";
val P = read_prop "phi";
in
- store_standard_thm_open (Binding.make ("equal_elim_rule1", @{here}))
+ store_standard_thm_open (Binding.make ("equal_elim_rule1", \<^here>))
(Thm.equal_elim (Thm.assume eq) (Thm.assume P) |> implies_intr_list [eq, P])
end;
(* PROP ?psi == PROP ?phi ==> PROP ?phi ==> PROP ?psi *)
val equal_elim_rule2 =
- store_standard_thm_open (Binding.make ("equal_elim_rule2", @{here}))
+ store_standard_thm_open (Binding.make ("equal_elim_rule2", \<^here>))
(symmetric_thm RS equal_elim_rule1);
(* PROP ?phi ==> PROP ?phi ==> PROP ?psi ==> PROP ?psi *)
@@ -561,7 +561,7 @@
val P = read_prop "phi";
val Q = read_prop "psi";
val thm = implies_intr_list [P, P, Q] (Thm.assume Q);
- in store_standard_thm_open (Binding.make ("remdups_rl", @{here})) thm end;
+ in store_standard_thm_open (Binding.make ("remdups_rl", \<^here>)) thm end;
@@ -583,15 +583,15 @@
val protect = Thm.apply (certify Logic.protectC);
val protectI =
- store_standard_thm (Binding.concealed (Binding.make ("protectI", @{here})))
+ store_standard_thm (Binding.concealed (Binding.make ("protectI", \<^here>)))
(Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A));
val protectD =
- store_standard_thm (Binding.concealed (Binding.make ("protectD", @{here})))
+ store_standard_thm (Binding.concealed (Binding.make ("protectD", \<^here>)))
(Thm.equal_elim prop_def (Thm.assume (protect A)));
val protect_cong =
- store_standard_thm_open (Binding.make ("protect_cong", @{here}))
+ store_standard_thm_open (Binding.make ("protect_cong", \<^here>))
(Thm.reflexive (protect A));
fun implies_intr_protected asms th =
@@ -606,7 +606,7 @@
(* term *)
val termI =
- store_standard_thm (Binding.concealed (Binding.make ("termI", @{here})))
+ store_standard_thm (Binding.concealed (Binding.make ("termI", \<^here>)))
(Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A)));
fun mk_term ct =
@@ -637,11 +637,11 @@
| is_sort_constraint _ = false;
val sort_constraintI =
- store_standard_thm (Binding.concealed (Binding.make ("sort_constraintI", @{here})))
+ store_standard_thm (Binding.concealed (Binding.make ("sort_constraintI", \<^here>)))
(Thm.equal_elim (Thm.symmetric sort_constraint_def) (mk_term T));
val sort_constraint_eq =
- store_standard_thm (Binding.concealed (Binding.make ("sort_constraint_eq", @{here})))
+ store_standard_thm (Binding.concealed (Binding.make ("sort_constraint_eq", \<^here>)))
(Thm.equal_intr
(Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA)
(Thm.unvarify_global (Context.the_global_context ()) sort_constraintI)))
@@ -676,7 +676,7 @@
|> Thm.forall_intr cx
|> Thm.implies_intr cphi
|> Thm.implies_intr rhs)
- |> store_standard_thm_open (Binding.make ("norm_hhf_eq", @{here}))
+ |> store_standard_thm_open (Binding.make ("norm_hhf_eq", \<^here>))
end;
val norm_hhf_prop = Logic.dest_equals (Thm.prop_of norm_hhf_eq);
--- a/src/Pure/goal.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/goal.ML Tue Dec 13 11:51:42 2016 +0100
@@ -255,7 +255,7 @@
(* skip proofs *)
-val quick_and_dirty_raw = Config.declare_option ("quick_and_dirty", @{here});
+val quick_and_dirty_raw = Config.declare_option ("quick_and_dirty", \<^here>);
val quick_and_dirty = Config.bool quick_and_dirty_raw;
fun prove_sorry ctxt xs asms prop tac =
--- a/src/Pure/goal_display.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/goal_display.ML Tue Dec 13 11:51:42 2016 +0100
@@ -19,10 +19,10 @@
structure Goal_Display: GOAL_DISPLAY =
struct
-val goals_limit_raw = Config.declare_option ("goals_limit", @{here});
+val goals_limit_raw = Config.declare_option ("goals_limit", \<^here>);
val goals_limit = Config.int goals_limit_raw;
-val show_main_goal_raw = Config.declare_option ("show_main_goal", @{here});
+val show_main_goal_raw = Config.declare_option ("show_main_goal", \<^here>);
val show_main_goal = Config.bool show_main_goal_raw;
--- a/src/Pure/more_thm.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/more_thm.ML Tue Dec 13 11:51:42 2016 +0100
@@ -654,13 +654,13 @@
(* options *)
-val show_consts_raw = Config.declare_option ("show_consts", @{here});
+val show_consts_raw = Config.declare_option ("show_consts", \<^here>);
val show_consts = Config.bool show_consts_raw;
-val show_hyps_raw = Config.declare ("show_hyps", @{here}) (fn _ => Config.Bool false);
+val show_hyps_raw = Config.declare ("show_hyps", \<^here>) (fn _ => Config.Bool false);
val show_hyps = Config.bool show_hyps_raw;
-val show_tags_raw = Config.declare ("show_tags", @{here}) (fn _ => Config.Bool false);
+val show_tags_raw = Config.declare ("show_tags", \<^here>) (fn _ => Config.Bool false);
val show_tags = Config.bool show_tags_raw;
--- a/src/Pure/pattern.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/pattern.ML Tue Dec 13 11:51:42 2016 +0100
@@ -31,7 +31,7 @@
exception Pattern;
val unify_trace_failure_raw =
- Config.declare ("unify_trace_failure", @{here}) (fn _ => Config.Bool false);
+ Config.declare ("unify_trace_failure", \<^here>) (fn _ => Config.Bool false);
val unify_trace_failure = Config.bool unify_trace_failure_raw;
fun string_of_term ctxt env binders t =
--- a/src/Pure/pure_syn.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/pure_syn.ML Tue Dec 13 11:51:42 2016 +0100
@@ -16,49 +16,49 @@
val semi = Scan.option (Parse.$$$ ";");
val _ =
- Outer_Syntax.command ("chapter", @{here}) "chapter heading"
+ Outer_Syntax.command ("chapter", \<^here>) "chapter heading"
(Parse.opt_target -- Parse.document_source --| semi
>> Thy_Output.document_command {markdown = false});
val _ =
- Outer_Syntax.command ("section", @{here}) "section heading"
+ Outer_Syntax.command ("section", \<^here>) "section heading"
(Parse.opt_target -- Parse.document_source --| semi
>> Thy_Output.document_command {markdown = false});
val _ =
- Outer_Syntax.command ("subsection", @{here}) "subsection heading"
+ Outer_Syntax.command ("subsection", \<^here>) "subsection heading"
(Parse.opt_target -- Parse.document_source --| semi
>> Thy_Output.document_command {markdown = false});
val _ =
- Outer_Syntax.command ("subsubsection", @{here}) "subsubsection heading"
+ Outer_Syntax.command ("subsubsection", \<^here>) "subsubsection heading"
(Parse.opt_target -- Parse.document_source --| semi
>> Thy_Output.document_command {markdown = false});
val _ =
- Outer_Syntax.command ("paragraph", @{here}) "paragraph heading"
+ Outer_Syntax.command ("paragraph", \<^here>) "paragraph heading"
(Parse.opt_target -- Parse.document_source --| semi
>> Thy_Output.document_command {markdown = false});
val _ =
- Outer_Syntax.command ("subparagraph", @{here}) "subparagraph heading"
+ Outer_Syntax.command ("subparagraph", \<^here>) "subparagraph heading"
(Parse.opt_target -- Parse.document_source --| semi
>> Thy_Output.document_command {markdown = false});
val _ =
- Outer_Syntax.command ("text", @{here}) "formal comment (primary style)"
+ Outer_Syntax.command ("text", \<^here>) "formal comment (primary style)"
(Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true});
val _ =
- Outer_Syntax.command ("txt", @{here}) "formal comment (secondary style)"
+ Outer_Syntax.command ("txt", \<^here>) "formal comment (secondary style)"
(Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true});
val _ =
- Outer_Syntax.command ("text_raw", @{here}) "LaTeX text (without surrounding environment)"
+ Outer_Syntax.command ("text_raw", \<^here>) "LaTeX text (without surrounding environment)"
(Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true});
val _ =
- Outer_Syntax.command ("theory", @{here}) "begin theory"
+ Outer_Syntax.command ("theory", \<^here>) "begin theory"
(Thy_Header.args >>
(fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization")));
--- a/src/Pure/pure_thy.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/pure_thy.ML Tue Dec 13 11:51:42 2016 +0100
@@ -67,16 +67,16 @@
(Sign.map_naming (Name_Space.set_theory_name Context.PureN) #>
Old_Appl_Syntax.put false #>
Sign.add_types_global
- [(Binding.make ("fun", @{here}), 2, NoSyn),
- (Binding.make ("prop", @{here}), 0, NoSyn),
- (Binding.make ("itself", @{here}), 1, NoSyn),
- (Binding.make ("dummy", @{here}), 0, NoSyn)]
+ [(Binding.make ("fun", \<^here>), 2, NoSyn),
+ (Binding.make ("prop", \<^here>), 0, NoSyn),
+ (Binding.make ("itself", \<^here>), 1, NoSyn),
+ (Binding.make ("dummy", \<^here>), 0, NoSyn)]
#> Theory.add_deps_global "fun" ((Defs.Type, "fun"), [typ "'a", typ "'b"]) []
#> Theory.add_deps_global "prop" ((Defs.Type, "prop"), []) []
#> Theory.add_deps_global "itself" ((Defs.Type, "itself"), [typ "'a"]) []
#> Theory.add_deps_global "dummy" ((Defs.Type, "dummy"), []) []
#> Sign.add_nonterminals_global
- (map (fn name => Binding.make (name, @{here}))
+ (map (fn name => Binding.make (name, \<^here>))
(Lexicon.terminals @ ["logic", "type", "types", "sort", "classes",
"args", "cargs", "pttrn", "pttrns", "idt", "idts", "aprop", "asms",
"any", "prop'", "num_const", "float_const", "num_position",
@@ -194,12 +194,12 @@
#> Sign.add_syntax ("", false)
[(const "Pure.prop", typ "prop => prop", mixfix ("_", [0], 0))]
#> Sign.add_consts
- [(qualify (Binding.make ("eq", @{here})), typ "'a => 'a => prop", infix_ ("\<equiv>", 2)),
- (qualify (Binding.make ("imp", @{here})), typ "prop => prop => prop", infixr_ ("\<Longrightarrow>", 1)),
- (qualify (Binding.make ("all", @{here})), typ "('a => prop) => prop", binder ("\<And>", 0, 0)),
- (qualify (Binding.make ("prop", @{here})), typ "prop => prop", NoSyn),
- (qualify (Binding.make ("type", @{here})), typ "'a itself", NoSyn),
- (qualify (Binding.make ("dummy_pattern", @{here})), typ "'a", Mixfix.mixfix "'_")]
+ [(qualify (Binding.make ("eq", \<^here>)), typ "'a => 'a => prop", infix_ ("\<equiv>", 2)),
+ (qualify (Binding.make ("imp", \<^here>)), typ "prop => prop => prop", infixr_ ("\<Longrightarrow>", 1)),
+ (qualify (Binding.make ("all", \<^here>)), typ "('a => prop) => prop", binder ("\<And>", 0, 0)),
+ (qualify (Binding.make ("prop", \<^here>)), typ "prop => prop", NoSyn),
+ (qualify (Binding.make ("type", \<^here>)), typ "'a itself", NoSyn),
+ (qualify (Binding.make ("dummy_pattern", \<^here>)), typ "'a", Mixfix.mixfix "'_")]
#> Theory.add_deps_global "Pure.eq" ((Defs.Const, "Pure.eq"), [typ "'a"]) []
#> Theory.add_deps_global "Pure.imp" ((Defs.Const, "Pure.imp"), []) []
#> Theory.add_deps_global "Pure.all" ((Defs.Const, "Pure.all"), [typ "'a"]) []
@@ -209,21 +209,21 @@
#> Sign.parse_translation Syntax_Trans.pure_parse_translation
#> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation
#> Sign.add_consts
- [(qualify (Binding.make ("term", @{here})), typ "'a => prop", NoSyn),
- (qualify (Binding.make ("sort_constraint", @{here})), typ "'a itself => prop", NoSyn),
- (qualify (Binding.make ("conjunction", @{here})), typ "prop => prop => prop", NoSyn)]
+ [(qualify (Binding.make ("term", \<^here>)), typ "'a => prop", NoSyn),
+ (qualify (Binding.make ("sort_constraint", \<^here>)), typ "'a itself => prop", NoSyn),
+ (qualify (Binding.make ("conjunction", \<^here>)), typ "prop => prop => prop", NoSyn)]
#> Sign.local_path
#> (Global_Theory.add_defs false o map Thm.no_attributes)
- [(Binding.make ("prop_def", @{here}),
+ [(Binding.make ("prop_def", \<^here>),
prop "(CONST Pure.prop :: prop => prop) (A::prop) == A::prop"),
- (Binding.make ("term_def", @{here}),
+ (Binding.make ("term_def", \<^here>),
prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"),
- (Binding.make ("sort_constraint_def", @{here}),
+ (Binding.make ("sort_constraint_def", \<^here>),
prop "(CONST Pure.sort_constraint :: 'a itself => prop) (CONST Pure.type :: 'a itself) ==\
\ (CONST Pure.term :: 'a itself => prop) (CONST Pure.type :: 'a itself)"),
- (Binding.make ("conjunction_def", @{here}),
+ (Binding.make ("conjunction_def", \<^here>),
prop "(A &&& B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd
#> fold (fn (a, prop) =>
- snd o Thm.add_axiom_global (Binding.make (a, @{here}), prop)) Proofterm.equality_axms);
+ snd o Thm.add_axiom_global (Binding.make (a, \<^here>), prop)) Proofterm.equality_axms);
end;
--- a/src/Pure/raw_simplifier.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/raw_simplifier.ML Tue Dec 13 11:51:42 2016 +0100
@@ -389,11 +389,11 @@
(* simp depth *)
-val simp_depth_limit_raw = Config.declare ("simp_depth_limit", @{here}) (K (Config.Int 100));
+val simp_depth_limit_raw = Config.declare ("simp_depth_limit", \<^here>) (K (Config.Int 100));
val simp_depth_limit = Config.int simp_depth_limit_raw;
val simp_trace_depth_limit_raw =
- Config.declare ("simp_trace_depth_limit", @{here}) (fn _ => Config.Int 1);
+ Config.declare ("simp_trace_depth_limit", \<^here>) (fn _ => Config.Int 1);
val simp_trace_depth_limit = Config.int simp_trace_depth_limit_raw;
fun inc_simp_depth ctxt =
@@ -412,10 +412,10 @@
exception SIMPLIFIER of string * thm list;
-val simp_debug_raw = Config.declare ("simp_debug", @{here}) (K (Config.Bool false));
+val simp_debug_raw = Config.declare ("simp_debug", \<^here>) (K (Config.Bool false));
val simp_debug = Config.bool simp_debug_raw;
-val simp_trace_raw = Config.declare ("simp_trace", @{here}) (fn _ => Config.Bool false);
+val simp_trace_raw = Config.declare ("simp_trace", \<^here>) (fn _ => Config.Bool false);
val simp_trace = Config.bool simp_trace_raw;
fun cond_warning ctxt msg =
--- a/src/Pure/simplifier.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/simplifier.ML Tue Dec 13 11:51:42 2016 +0100
@@ -332,23 +332,23 @@
(** method syntax **)
val cong_modifiers =
- [Args.$$$ congN -- Args.colon >> K (Method.modifier cong_add @{here}),
- Args.$$$ congN -- Args.add -- Args.colon >> K (Method.modifier cong_add @{here}),
- Args.$$$ congN -- Args.del -- Args.colon >> K (Method.modifier cong_del @{here})];
+ [Args.$$$ congN -- Args.colon >> K (Method.modifier cong_add \<^here>),
+ Args.$$$ congN -- Args.add -- Args.colon >> K (Method.modifier cong_add \<^here>),
+ Args.$$$ congN -- Args.del -- Args.colon >> K (Method.modifier cong_del \<^here>)];
val simp_modifiers =
- [Args.$$$ simpN -- Args.colon >> K (Method.modifier simp_add @{here}),
- Args.$$$ simpN -- Args.add -- Args.colon >> K (Method.modifier simp_add @{here}),
- Args.$$$ simpN -- Args.del -- Args.colon >> K (Method.modifier simp_del @{here}),
+ [Args.$$$ simpN -- Args.colon >> K (Method.modifier simp_add \<^here>),
+ Args.$$$ simpN -- Args.add -- Args.colon >> K (Method.modifier simp_add \<^here>),
+ Args.$$$ simpN -- Args.del -- Args.colon >> K (Method.modifier simp_del \<^here>),
Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon >>
- K {init = Raw_Simplifier.clear_simpset, attribute = simp_add, pos = @{here}}]
+ K {init = Raw_Simplifier.clear_simpset, attribute = simp_add, pos = \<^here>}]
@ cong_modifiers;
val simp_modifiers' =
- [Args.add -- Args.colon >> K (Method.modifier simp_add @{here}),
- Args.del -- Args.colon >> K (Method.modifier simp_del @{here}),
+ [Args.add -- Args.colon >> K (Method.modifier simp_add \<^here>),
+ Args.del -- Args.colon >> K (Method.modifier simp_del \<^here>),
Args.$$$ onlyN -- Args.colon >>
- K {init = Raw_Simplifier.clear_simpset, attribute = simp_add, pos = @{here}}]
+ K {init = Raw_Simplifier.clear_simpset, attribute = simp_add, pos = \<^here>}]
@ cong_modifiers;
val simp_options =
--- a/src/Pure/skip_proof.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/skip_proof.ML Tue Dec 13 11:51:42 2016 +0100
@@ -27,7 +27,7 @@
val (_, make_thm_cterm) =
Context.>>>
- (Context.map_theory_result (Thm.add_oracle (Binding.make ("skip_proof", @{here}), I)));
+ (Context.map_theory_result (Thm.add_oracle (Binding.make ("skip_proof", \<^here>), I)));
fun make_thm thy prop = make_thm_cterm (Thm.global_cterm_of thy prop);
--- a/src/Pure/type_infer.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/type_infer.ML Tue Dec 13 11:51:42 2016 +0100
@@ -101,7 +101,7 @@
(* fixate -- introduce fresh type variables *)
val object_logic =
- Config.bool (Config.declare ("Type_Infer.object_logic", @{here}) (K (Config.Bool true)));
+ Config.bool (Config.declare ("Type_Infer.object_logic", \<^here>) (K (Config.Bool true)));
fun fixate ctxt pattern ts =
let
--- a/src/Pure/type_infer_context.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/type_infer_context.ML Tue Dec 13 11:51:42 2016 +0100
@@ -21,7 +21,7 @@
(* constraints *)
val const_sorts =
- Config.bool (Config.declare ("const_sorts", @{here}) (K (Config.Bool true)));
+ Config.bool (Config.declare ("const_sorts", \<^here>) (K (Config.Bool true)));
fun const_type ctxt =
try ((not (Config.get ctxt const_sorts) ? Type.strip_sorts) o
--- a/src/Pure/unify.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/unify.ML Tue Dec 13 11:51:42 2016 +0100
@@ -32,19 +32,19 @@
(*Unification options*)
(*tracing starts above this depth, 0 for full*)
-val trace_bound_raw = Config.declare ("unify_trace_bound", @{here}) (K (Config.Int 50));
+val trace_bound_raw = Config.declare ("unify_trace_bound", \<^here>) (K (Config.Int 50));
val trace_bound = Config.int trace_bound_raw;
(*unification quits above this depth*)
-val search_bound_raw = Config.declare ("unify_search_bound", @{here}) (K (Config.Int 60));
+val search_bound_raw = Config.declare ("unify_search_bound", \<^here>) (K (Config.Int 60));
val search_bound = Config.int search_bound_raw;
(*print dpairs before calling SIMPL*)
-val trace_simp_raw = Config.declare ("unify_trace_simp", @{here}) (K (Config.Bool false));
+val trace_simp_raw = Config.declare ("unify_trace_simp", \<^here>) (K (Config.Bool false));
val trace_simp = Config.bool trace_simp_raw;
(*announce potential incompleteness of type unification*)
-val trace_types_raw = Config.declare ("unify_trace_types", @{here}) (K (Config.Bool false));
+val trace_types_raw = Config.declare ("unify_trace_types", \<^here>) (K (Config.Bool false));
val trace_types = Config.bool trace_types_raw;
--- a/src/Pure/variable.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Pure/variable.ML Tue Dec 13 11:51:42 2016 +0100
@@ -335,7 +335,7 @@
(* inner body mode *)
val inner_body =
- Config.bool (Config.declare ("inner_body", @{here}) (K (Config.Bool false)));
+ Config.bool (Config.declare ("inner_body", \<^here>) (K (Config.Bool false)));
fun is_body ctxt = Config.get ctxt inner_body;
val set_body = Config.put inner_body;
@@ -345,7 +345,7 @@
(* proper mode *)
val proper_fixes =
- Config.bool (Config.declare ("proper_fixes", @{here}) (K (Config.Bool true)));
+ Config.bool (Config.declare ("proper_fixes", \<^here>) (K (Config.Bool true)));
val improper_fixes = Config.put proper_fixes false;
fun restore_proper_fixes ctxt = Config.put proper_fixes (Config.get ctxt proper_fixes);
@@ -645,7 +645,7 @@
(* focus on outermost parameters: !!x y z. B *)
val bound_focus =
- Config.bool (Config.declare ("bound_focus", @{here}) (K (Config.Bool false)));
+ Config.bool (Config.declare ("bound_focus", \<^here>) (K (Config.Bool false)));
fun is_bound_focus ctxt = Config.get ctxt bound_focus;
val set_bound_focus = Config.put bound_focus;
--- a/src/Sequents/prover.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Sequents/prover.ML Tue Dec 13 11:51:42 2016 +0100
@@ -106,8 +106,8 @@
fun method tac =
Method.sections
- [Args.$$$ "add" -- Args.bang_colon >> K (Method.modifier safe_add @{here}),
- Args.$$$ "add" -- Args.colon >> K (Method.modifier unsafe_add @{here})]
+ [Args.$$$ "add" -- Args.bang_colon >> K (Method.modifier safe_add \<^here>),
+ Args.$$$ "add" -- Args.colon >> K (Method.modifier unsafe_add \<^here>)]
>> K (SIMPLE_METHOD' o tac);
--- a/src/Tools/intuitionistic.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/Tools/intuitionistic.ML Tue Dec 13 11:51:42 2016 +0100
@@ -78,13 +78,13 @@
>> (fn arg => Method.modifier (att arg) pos);
val modifiers =
- [modifier destN Args.bang_colon Args.bang Context_Rules.dest_bang @{here},
- modifier destN Args.colon (Scan.succeed ()) Context_Rules.dest @{here},
- modifier elimN Args.bang_colon Args.bang Context_Rules.elim_bang @{here},
- modifier elimN Args.colon (Scan.succeed ()) Context_Rules.elim @{here},
- modifier introN Args.bang_colon Args.bang Context_Rules.intro_bang @{here},
- modifier introN Args.colon (Scan.succeed ()) Context_Rules.intro @{here},
- Args.del -- Args.colon >> K (Method.modifier Context_Rules.rule_del @{here})];
+ [modifier destN Args.bang_colon Args.bang Context_Rules.dest_bang \<^here>,
+ modifier destN Args.colon (Scan.succeed ()) Context_Rules.dest \<^here>,
+ modifier elimN Args.bang_colon Args.bang Context_Rules.elim_bang \<^here>,
+ modifier elimN Args.colon (Scan.succeed ()) Context_Rules.elim \<^here>,
+ modifier introN Args.bang_colon Args.bang Context_Rules.intro_bang \<^here>,
+ modifier introN Args.colon (Scan.succeed ()) Context_Rules.intro \<^here>,
+ Args.del -- Args.colon >> K (Method.modifier Context_Rules.rule_del \<^here>)];
in
--- a/src/ZF/Tools/typechk.ML Mon Dec 12 17:40:06 2016 +0100
+++ b/src/ZF/Tools/typechk.ML Tue Dec 13 11:51:42 2016 +0100
@@ -120,8 +120,8 @@
"declaration of type-checking rule" #>
Method.setup @{binding typecheck}
(Method.sections
- [Args.add -- Args.colon >> K (Method.modifier TC_add @{here}),
- Args.del -- Args.colon >> K (Method.modifier TC_del @{here})]
+ [Args.add -- Args.colon >> K (Method.modifier TC_add \<^here>),
+ Args.del -- Args.colon >> K (Method.modifier TC_del \<^here>)]
>> K (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt))))
"ZF type-checking");