# HG changeset patch
# User wenzelm
# Date 1257179438 -3600
# Node ID cd6023a9a922a74843f7cd87785db722b420d4b2
# Parent  b834b42e4aa1d5e6aad880a38674d74d50f207e4
DEEPEN: all tracing is subject to trace_DEEPEN (NB: Proof General tends to "popup" tracing output);

diff -r b834b42e4aa1 -r cd6023a9a922 src/Pure/search.ML
--- a/src/Pure/search.ML	Mon Nov 02 17:29:48 2009 +0100
+++ b/src/Pure/search.ML	Mon Nov 02 17:30:38 2009 +0100
@@ -178,13 +178,16 @@
 val trace_DEEPEN = Unsynchronized.ref false;
 
 fun DEEPEN (inc,lim) tacf m i =
-  let fun dpn m st =
-       st |> (if has_fewer_prems i st then no_tac
-              else if m>lim then
-                       (tracing "Search depth limit exceeded: giving up";
-                        no_tac)
-              else (if !trace_DEEPEN then tracing ("Search depth = " ^ string_of_int m) else ();
-                             tacf m i  ORELSE  dpn (m+inc)))
+  let
+    fun dpn m st =
+      st |>
+       (if has_fewer_prems i st then no_tac
+        else if m>lim then
+          (if !trace_DEEPEN then tracing "Search depth limit exceeded: giving up" else ();
+            no_tac)
+        else
+          (if !trace_DEEPEN then tracing ("Search depth = " ^ string_of_int m) else ();
+            tacf m i  ORELSE  dpn (m+inc)))
   in  dpn m  end;