--- 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)