reduced simp_depth_limit
authornipkow
Sun Oct 29 07:46:28 2017 +0100 (18 months ago)
changeset 66934b86513bcf7ac
parent 66933 4e06b030730c
child 66935 d0f12783cd80
reduced simp_depth_limit
src/Pure/raw_simplifier.ML
     1.1 --- a/src/Pure/raw_simplifier.ML	Sat Oct 28 23:32:37 2017 +0200
     1.2 +++ b/src/Pure/raw_simplifier.ML	Sun Oct 29 07:46:28 2017 +0100
     1.3 @@ -389,7 +389,13 @@
     1.4  
     1.5  (* simp depth *)
     1.6  
     1.7 -val simp_depth_limit_raw = Config.declare ("simp_depth_limit", \<^here>) (K (Config.Int 100));
     1.8 +(*
     1.9 +The simp_depth_limit is meant to abort infinite recursion of the simplifier
    1.10 +early but should not terminate "normal" executions.
    1.11 +As of 2017, 25 would suffice; 40 builds in a safety margin.
    1.12 +*)
    1.13 +
    1.14 +val simp_depth_limit_raw = Config.declare ("simp_depth_limit", \<^here>) (K (Config.Int 40));
    1.15  val simp_depth_limit = Config.int simp_depth_limit_raw;
    1.16  
    1.17  val simp_trace_depth_limit_raw =