src/Pure/meta_simplifier.ML

 
 signature BASIC_META_SIMPLIFIER =
 sig
   val debug_simp: bool ref
   val trace_simp: bool ref
-  val simp_depth_limit: int ref
   val trace_simp_depth_limit: int ref
   type rrule
   val eq_rrule: rrule * rrule -> bool
   type cong
   type simpset

 signature META_SIMPLIFIER =
 sig
   include BASIC_META_SIMPLIFIER
   exception SIMPLIFIER of string * thm
   val solver: simpset -> solver -> int -> tactic
+  val simp_depth_limit_value: Config.value Config.T
+  val simp_depth_limit: int Config.T
   val clear_ss: simpset -> simpset
   val simproc_i: theory -> string -> term list
     -> (theory -> simpset -> term -> thm option) -> simproc
   val simproc: theory -> string -> string list
     -> (theory -> simpset -> term -> thm option) -> simproc

 fun eq_solver (Solver {id = id1, ...}, Solver {id = id2, ...}) = (id1 = id2);
 
 
 (* simp depth *)
 
-val simp_depth_limit = ref 100;
+val simp_depth_limit_value = Config.declare false "simp_depth_limit" (Config.Int 100);
+val simp_depth_limit = Config.int simp_depth_limit_value;
+
 val trace_simp_depth_limit = ref 1;
 
 fun trace_depth (Simpset ({depth = (depth, exceeded), ...}, _)) msg =
   if depth > ! trace_simp_depth_limit then
     if ! exceeded then () else (tracing "trace_simp_depth_limit exceeded!"; exceeded := true)

   IMPORTANT: rewrite rules must not introduce new Vars or TVars!
 *)
 
 fun rewritec (prover, thyt, maxt) ss t =
   let
+    val ctxt = the_context ss;
     val Simpset ({rules, ...}, {congs, procs, termless, ...}) = ss;
     val eta_thm = Thm.eta_conversion t;
     val eta_t' = Thm.rhs_of eta_thm;
     val eta_t = term_of eta_t';
     fun rew {thm, name, lhs, elhs, extra, fo, perm} =

               let val lr = Logic.dest_equals prop;
                   val SOME thm'' = check_conv false ss eta_thm thm'
               in SOME (thm'', uncond_skel (congs, lr)) end)
            else
              (trace_thm (fn () => "Trying to rewrite:") ss thm';
-              if simp_depth ss > ! simp_depth_limit
+              if simp_depth ss > Config.get ctxt simp_depth_limit
               then let val s = "simp_depth_limit exceeded - giving up"
                    in trace false (fn () => s) ss; warning s; NONE end
               else
               case prover ss thm' of
                 NONE => (trace_thm (fn () => "FAILED") ss thm'; NONE)