# HG changeset patch
# User wenzelm
# Date 1481626302 -3600
# Node ID 851ae0e7b09cefce572a100698c455928eb6450a
# Parent  628b271c5b8bc8843cf43b6a36cac870ff4be167
more symbols;

diff -r 628b271c5b8b -r 851ae0e7b09c etc/symbols
--- 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
diff -r 628b271c5b8b -r 851ae0e7b09c lib/texinputs/isabellesym.sty
--- 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}\ }
diff -r 628b271c5b8b -r 851ae0e7b09c src/HOL/Library/old_recdef.ML
--- 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;
 
 
diff -r 628b271c5b8b -r 851ae0e7b09c src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
--- 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
diff -r 628b271c5b8b -r 851ae0e7b09c src/Provers/clasimp.ML
--- 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 @
diff -r 628b271c5b8b -r 851ae0e7b09c src/Provers/classical.ML
--- 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);
diff -r 628b271c5b8b -r 851ae0e7b09c src/Provers/splitter.ML
--- 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
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/General/name_space.ML
--- 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 =
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/General/position.ML
--- 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
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/Isar/attrib.ML
--- 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");
 
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/Isar/local_defs.ML
--- 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
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/Isar/method.ML
--- 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
 
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/Isar/outer_syntax.ML
--- 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 () =>
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/Isar/proof_context.ML
--- 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 []
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/ML/ml_antiquotation.ML
--- 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)))));
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/ML/ml_compiler0.ML
--- 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" :: #"_" ::
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/ML/ml_env.ML
--- 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
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/ML/ml_options.ML
--- 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 =
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/ML/ml_print_depth.ML
--- 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;
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/Proof/extraction.ML
--- 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);
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/Proof/proof_syntax.ML
--- 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)),
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/Proof/reconstruct.ML
--- 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 ());
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/Syntax/ast.ML
--- 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 =
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/Syntax/parser.ML
--- 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*)
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/Syntax/printer.ML
--- 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
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/Syntax/syntax.ML
--- 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;
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/Syntax/syntax_trans.ML
--- 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 =
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/Thy/thy_header.ML
--- 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 *)
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/Thy/thy_output.ML
--- 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
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/Tools/find_consts.ML
--- 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
 
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/Tools/find_theorems.ML
--- 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
 
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/conjunction.ML
--- 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)
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/drule.ML
--- 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);
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/goal.ML
--- 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 =
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/goal_display.ML
--- 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;
 
 
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/more_thm.ML
--- 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;
 
 
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/pattern.ML
--- 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 =
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/pure_syn.ML
--- 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")));
 
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/pure_thy.ML
--- 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;
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/raw_simplifier.ML
--- 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 =
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/simplifier.ML
--- 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 =
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/skip_proof.ML
--- 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);
 
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/type_infer.ML
--- 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
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/type_infer_context.ML
--- 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
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/unify.ML
--- 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;
 
 
diff -r 628b271c5b8b -r 851ae0e7b09c src/Pure/variable.ML
--- 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;
diff -r 628b271c5b8b -r 851ae0e7b09c src/Sequents/prover.ML
--- 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);
 
 
diff -r 628b271c5b8b -r 851ae0e7b09c src/Tools/intuitionistic.ML
--- 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
 
diff -r 628b271c5b8b -r 851ae0e7b09c src/ZF/Tools/typechk.ML
--- 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");