changeset 35380 | 6ac5b81a763d |
parent 35378 | 95d0e3adf38e |
child 35537 | 59dd6be5834c |
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Thu Feb 25 10:04:50 2010 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Thu Feb 25 14:01:34 2010 +0100 @@ -217,7 +217,7 @@ fun try' j = if j <= i then let - val _ = priority ("Executing depth " ^ string_of_int j) + val _ = if quiet then () else priority ("Executing depth " ^ string_of_int j) in case f j handle Match => (if quiet then () else warning "Exception Match raised during quickcheck"; NONE)