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 =