diff -r 2e873c5f0e2c -r 998af7667fa3 src/Pure/search.ML
--- a/src/Pure/search.ML	Tue Oct 20 16:33:13 1998 +0200
+++ b/src/Pure/search.ML	Tue Oct 20 16:33:47 1998 +0200
@@ -32,6 +32,7 @@
   val THEN_ASTAR	: tactic -> (thm->bool) * (int->thm->int) -> tactic
 			  -> tactic
   val BREADTH_FIRST	: (thm -> bool) -> tactic -> tactic
+  val QUIET_BREADTH_FIRST	: (thm -> bool) -> tactic -> tactic
   end;
 
 structure Search : SEARCH = 
@@ -214,17 +215,20 @@
 
 (*Breadth-first search to satisfy satpred (including initial state) 
   SLOW -- SHOULD NOT USE APPEND!*)
-fun BREADTH_FIRST satpred tac = 
+fun gen_BREADTH_FIRST message satpred (tac:tactic) = 
   let val tacf = Seq.list_of o tac;
       fun bfs prfs =
 	 (case  partition satpred prfs  of
 	      ([],[]) => []
 	    | ([],nonsats) => 
-		  (prs("breadth=" ^ string_of_int(length nonsats) ^ "\n");
+		  (message("breadth=" ^ string_of_int(length nonsats) ^ "\n");
 		   bfs (List.concat (map tacf nonsats)))
 	    | (sats,_)  => sats)
   in (fn st => Seq.of_list (bfs [st])) end;
 
+val BREADTH_FIRST = gen_BREADTH_FIRST prs;
+val QUIET_BREADTH_FIRST = gen_BREADTH_FIRST (K ());
+
 
 (*  Author: 	Norbert Voelker, FernUniversitaet Hagen
     Remarks:    Implementation of A*-like proof procedure by modification