be less verbose about simplification depth
authorkleing
Tue May 20 11:52:42 2003 +0200 (2003-05-20)
changeset 140408a2c8f762837
parent 14039 bb70604a07c4
child 14041 c2d981d222bf
be less verbose about simplification depth
src/Pure/meta_simplifier.ML
     1.1 --- a/src/Pure/meta_simplifier.ML	Sun May 18 16:30:20 2003 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Tue May 20 11:52:42 2003 +0200
     1.3 @@ -193,7 +193,7 @@
     1.4    let val depth1 = depth+1
     1.5    in if depth1 > !simp_depth_limit
     1.6       then (warning "simp_depth_limit exceeded - giving up"; None)
     1.7 -     else (if depth1 mod 5 = 0
     1.8 +     else (if depth1 mod 10 = 0
     1.9             then warning("Simplification depth " ^ string_of_int depth1)
    1.10             else ();
    1.11             Some(mk_mss(rules,congs,procs,bounds,prems,mk_rews,termless,depth1))