# HG changeset patch
# User kleing
# Date 1053424362 -7200
# Node ID 8a2c8f762837e66d210eb8d062de5475a949cbb4
# Parent  bb70604a07c4dcfdc9594d6078d270add7ef052d
be less verbose about simplification depth

diff -r bb70604a07c4 -r 8a2c8f762837 src/Pure/meta_simplifier.ML
--- 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))