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