diff -r 9bcecd429f77 -r 234ec7011e5d src/HOL/Library/SML_Quickcheck.thy --- a/src/HOL/Library/SML_Quickcheck.thy Tue Mar 29 23:46:46 2011 +0200 +++ b/src/HOL/Library/SML_Quickcheck.thy Wed Mar 30 09:44:16 2011 +0200 @@ -8,7 +8,7 @@ setup {* Inductive_Codegen.quickcheck_setup #> Context.theory_map (Quickcheck.add_generator ("SML", - fn ctxt => fn (t, eval_terms) => + fn ctxt => fn [(t, eval_terms)] => let val test_fun = Codegen.test_term ctxt t val iterations = Config.get ctxt Quickcheck.iterations @@ -21,7 +21,7 @@ in case result of NONE => iterate size (j - 1) | SOME q => SOME q end - in fn size => (iterate size iterations, NONE) end)) + in fn [size] => (iterate size iterations, NONE) end)) *} end