simp_depth warning now mod 20, not mod 10 (too often)
authornipkow
Tue, 16 Aug 2005 12:51:07 +0200
changeset 17046 8da7f68d0893
parent 17045 e108cd5b6986
child 17047 e2e2d75bb37b
simp_depth warning now mod 20, not mod 10 (too often)
src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Mon Aug 15 21:39:15 2005 +0200
+++ b/src/Pure/meta_simplifier.ML	Tue Aug 16 12:51:07 2005 +0200
@@ -1112,7 +1112,7 @@
 
 fun rewrite_cterm mode prover ss ct =
   (inc simp_depth;
-   if !simp_depth mod 10 = 0
+   if !simp_depth mod 20 = 0
    then warning ("Simplification depth " ^ string_of_int (!simp_depth))
    else ();
    trace_cterm false "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:" ss ct;