author | nipkow |
Tue, 16 Aug 2005 12:51:07 +0200 | |
changeset 17046 | 8da7f68d0893 |
parent 17045 | e108cd5b6986 |
child 17047 | e2e2d75bb37b |
--- 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;