src/Pure/meta_simplifier.ML

     prover: how to solve premises in conditional rewrites and congruences
 *)
 
 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;
    let val {thy, t, maxidx, ...} = Thm.rep_cterm ct
        val res = bottomc (mode, prover, thy, maxidx) ss ct