src/Pure/raw_simplifier.ML
changeset 56438 7f6b2634d853
parent 56245 84fc7dfa3cd4
child 57859 29e728588163
     1.1 --- a/src/Pure/raw_simplifier.ML	Sun Apr 06 15:51:02 2014 +0200
     1.2 +++ b/src/Pure/raw_simplifier.ML	Sun Apr 06 16:36:28 2014 +0200
     1.3 @@ -394,12 +394,13 @@
     1.4  
     1.5  (* simp depth *)
     1.6  
     1.7 -val simp_depth_limit_raw = Config.declare "simp_depth_limit" (K (Config.Int 100));
     1.8 +val simp_depth_limit_raw = Config.declare ("simp_depth_limit", @{here}) (K (Config.Int 100));
     1.9  val simp_depth_limit = Config.int simp_depth_limit_raw;
    1.10  
    1.11  val simp_trace_depth_limit_default = Unsynchronized.ref 1;
    1.12 -val simp_trace_depth_limit_raw = Config.declare "simp_trace_depth_limit"
    1.13 -  (fn _ => Config.Int (! simp_trace_depth_limit_default));
    1.14 +val simp_trace_depth_limit_raw =
    1.15 +  Config.declare ("simp_trace_depth_limit", @{here})
    1.16 +    (fn _ => Config.Int (! simp_trace_depth_limit_default));
    1.17  val simp_trace_depth_limit = Config.int simp_trace_depth_limit_raw;
    1.18  
    1.19  fun inc_simp_depth ctxt =
    1.20 @@ -418,11 +419,12 @@
    1.21  
    1.22  exception SIMPLIFIER of string * thm list;
    1.23  
    1.24 -val simp_debug_raw = Config.declare "simp_debug" (K (Config.Bool false));
    1.25 +val simp_debug_raw = Config.declare ("simp_debug", @{here}) (K (Config.Bool false));
    1.26  val simp_debug = Config.bool simp_debug_raw;
    1.27  
    1.28  val simp_trace_default = Unsynchronized.ref false;
    1.29 -val simp_trace_raw = Config.declare "simp_trace" (fn _ => Config.Bool (! simp_trace_default));
    1.30 +val simp_trace_raw =
    1.31 +  Config.declare ("simp_trace", @{here}) (fn _ => Config.Bool (! simp_trace_default));
    1.32  val simp_trace = Config.bool simp_trace_raw;
    1.33  
    1.34  fun cond_warning ctxt msg =