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;