diff -r 7cbebd636e79 -r 7ee65dbffa31 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Mon Oct 25 20:24:13 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Mon Oct 25 21:06:56 2010 +0200
@@ -327,7 +327,7 @@
     fun try' j =
       if j <= i then
         let
-          val _ = if quiet then () else priority ("Executing depth " ^ string_of_int j)
+          val _ = if quiet then () else Output.urgent_message ("Executing depth " ^ string_of_int j)
         in
           case f j handle Match => (if quiet then ()
              else warning "Exception Match raised during quickcheck"; NONE)