
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




