# HG changeset patch
# User bulwahn
# Date 1300468782 -3600
# Node ID da92153d6dff8acd502e54a43addbd9aa1d4cb00
# Parent  bd6515e113b257ffdc73578348944b3e97363e59
adapting SML_Quickcheck

diff -r bd6515e113b2 -r da92153d6dff src/HOL/Library/SML_Quickcheck.thy
--- a/src/HOL/Library/SML_Quickcheck.thy	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/Library/SML_Quickcheck.thy	Fri Mar 18 18:19:42 2011 +0100
@@ -8,7 +8,7 @@
 setup {*
   Inductive_Codegen.quickcheck_setup #>
   Context.theory_map (Quickcheck.add_generator ("SML",
-    fn ctxt => fn t =>
+    fn ctxt => fn (t, eval_terms) =>
       let
         val test_fun = Codegen.test_term ctxt t 
         val iterations = Config.get ctxt Quickcheck.iterations