--- a/src/HOL/Library/SML_Quickcheck.thy Wed Apr 20 14:33:33 2011 +0200
+++ b/src/HOL/Library/SML_Quickcheck.thy Wed Apr 20 15:55:34 2011 +0200
@@ -11,17 +11,17 @@
fn ctxt => fn [(t, eval_terms)] =>
let
val prop = list_abs_free (Term.add_frees t [], t)
- val test_fun = Codegen.test_term ctxt prop
+ val test_fun = Codegen.test_term ctxt prop
val iterations = Config.get ctxt Quickcheck.iterations
fun iterate size 0 = NONE
| iterate size j =
- let
- val result = test_fun size handle Match =>
- (if Config.get ctxt Quickcheck.quiet then ()
- else warning "Exception Match raised during quickcheck"; NONE)
- in
- case result of NONE => iterate size (j - 1) | SOME q => SOME q
- end
+ let
+ val result = test_fun size handle Match =>
+ (if Config.get ctxt Quickcheck.quiet then ()
+ else warning "Exception Match raised during quickcheck"; NONE)
+ in
+ case result of NONE => iterate size (j - 1) | SOME q => SOME q
+ end
in fn [_, size] => (iterate size iterations, NONE) end))
*}