src/Pure/search.ML

   val DEPTH_FIRST	: (thm -> bool) -> tactic -> tactic
   val DEPTH_SOLVE	: tactic -> tactic
   val DEPTH_SOLVE_1	: tactic -> tactic
   val ITER_DEEPEN	: (thm->bool) -> (int->tactic) -> tactic
   val THEN_ITER_DEEPEN	: tactic -> (thm->bool) -> (int->tactic) -> tactic
+  val iter_deepen_limit : int ref
 
   val has_fewer_prems	: int -> thm -> bool   
   val IF_UNSOLVED	: tactic -> tactic
   val SOLVE		: tactic -> tactic
   val DETERM_UNTIL_SOLVED: tactic -> tactic

 	        if np' < np then take (qs, (k,np,rgd,stq)::rqs)
 		            else arg
     in  prune_aux (take (qs, []))  end;
 
 
+(*No known example (on 1-5-2007) needs even thirty*)
+val iter_deepen_limit = ref 50;
+
 (*Depth-first iterative deepening search for a state that satisfies satp
   tactic tac0 sets up the initial goal queue, while tac1 searches it.
   The solution sequence is redundant: the cutoff heuristic makes it impossible
   to suppress solutions arising from earlier searches, as the accumulated cost
   (k) can be wrong.*)

  let val countr = ref 0
      and tf = tracify trace_DEPTH_FIRST (tac1 1)
      and qs0 = tac0 st
      (*bnd = depth bound; inc = estimate of increment required next*)
      fun depth (bnd,inc) [] = 
+          if bnd > !iter_deepen_limit then
+	     (tracing (string_of_int (!countr) ^ 
+		       " inferences so far.  Giving up at " ^ string_of_int bnd);
+	      NONE)
+          else
 	     (tracing (string_of_int (!countr) ^ 
 		       " inferences so far.  Searching to depth " ^ 
 		       string_of_int bnd);
 	      (*larger increments make it run slower for the hard problems*)
 	      depth (bnd+inc, 10)) [(0, 1, false, qs0)]
        | depth (bnd,inc) ((k,np,rgd,q)::qs) =
 	  if k>=bnd then depth (bnd,inc) qs
           else
 	  case (countr := !countr+1;
 		if !trace_DEPTH_FIRST then
-		    tracing (string_of_int np ^ 
-			     implode (map (fn _ => "*") qs))
+		    tracing (string_of_int np ^ implode (map (fn _ => "*") qs))
 		else ();
 		Seq.pull q) of
 	     NONE         => depth (bnd,inc) qs
 	   | SOME(st,stq) => 
 	       if satp st	(*solution!*)