trace_simp_depth_limit is 1 by default

--- a/src/Pure/meta_simplifier.ML	Wed Jan 04 16:37:57 2006 +0100
+++ b/src/Pure/meta_simplifier.ML	Wed Jan 04 16:38:40 2006 +0100
@@ -241,13 +241,17 @@
 val trace_simp = ref false;
 val simp_depth = ref 0;
 val simp_depth_limit = ref 100;
-val trace_simp_depth_limit = ref 100;
-
+val trace_simp_depth_limit = ref 1;
+val trace_simp_depth_limit_exceeded = ref false;
 local
 
 fun println a =
-  if ! simp_depth > ! trace_simp_depth_limit then ()
-  else tracing (enclose "[" "]" (string_of_int (! simp_depth)) ^ a);
+  if ! simp_depth > ! trace_simp_depth_limit
+  then if !trace_simp_depth_limit_exceeded then ()
+       else (tracing "trace_simp_depth_limit exceeded!";
+             trace_simp_depth_limit_exceeded := true)
+  else (tracing (enclose "[" "]" (string_of_int (! simp_depth)) ^ a);
+        trace_simp_depth_limit_exceeded := false);
 
 fun prnt warn a = if warn then warning a else println a;