--- 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 =