# HG changeset patch
# User nipkow
# Date 1509259588 -3600
# Node ID b86513bcf7acc88379ce923995b8b18366966125
# Parent  4e06b030730c72461b14f909f6bbb079bad726bf
reduced simp_depth_limit

diff -r 4e06b030730c -r b86513bcf7ac src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Sat Oct 28 23:32:37 2017 +0200
+++ b/src/Pure/raw_simplifier.ML	Sun Oct 29 07:46:28 2017 +0100
@@ -389,7 +389,13 @@
 
 (* simp depth *)
 
-val simp_depth_limit_raw = Config.declare ("simp_depth_limit", \<^here>) (K (Config.Int 100));
+(*
+The simp_depth_limit is meant to abort infinite recursion of the simplifier
+early but should not terminate "normal" executions.
+As of 2017, 25 would suffice; 40 builds in a safety margin.
+*)
+
+val simp_depth_limit_raw = Config.declare ("simp_depth_limit", \<^here>) (K (Config.Int 40));
 val simp_depth_limit = Config.int simp_depth_limit_raw;
 
 val simp_trace_depth_limit_raw =