src/Pure/search.ML
changeset 14160 6750ff1dfc32
parent 12262 11ff5f47df6e
child 15531 08c8dad8e399
--- a/src/Pure/search.ML	Wed Aug 20 13:34:17 2003 +0200
+++ b/src/Pure/search.ML	Thu Aug 21 11:41:44 2003 +0200
@@ -183,13 +183,15 @@
 (*Simple iterative deepening tactical.  It merely "deepens" any search tactic
   using increment "inc" up to limit "lim". *)
 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 "Giving up..."; no_tac)
-				 else (tracing ("Depth = " ^ string_of_int m);
-				       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 
+		       (warning "Search depth limit exceeded: giving up"; 
+			no_tac)
+	      else (warning ("Search depth = " ^ string_of_int m);
+			     tacf m i  ORELSE  dpn (m+inc)))
   in  dpn m  end;
-
+ 
 (*** Best-first search ***)
 
 val trace_BEST_FIRST = ref false;