author | kleing |
Tue, 20 May 2003 11:52:42 +0200 | |
changeset 14040 | 8a2c8f762837 |
parent 14039 | bb70604a07c4 |
child 14041 | c2d981d222bf |
--- a/src/Pure/meta_simplifier.ML Sun May 18 16:30:20 2003 +0200 +++ b/src/Pure/meta_simplifier.ML Tue May 20 11:52:42 2003 +0200 @@ -193,7 +193,7 @@ let val depth1 = depth+1 in if depth1 > !simp_depth_limit then (warning "simp_depth_limit exceeded - giving up"; None) - else (if depth1 mod 5 = 0 + else (if depth1 mod 10 = 0 then warning("Simplification depth " ^ string_of_int depth1) else (); Some(mk_mss(rules,congs,procs,bounds,prems,mk_rews,termless,depth1))