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;