diff -r 7ec150fcf3dc -r 5611f178a747 src/HOL/Library/SML_Quickcheck.thy --- 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)) *}