src/HOL/Library/Quickcheck.thy
changeset 30970 3fe2e418a071
parent 30945 0418e9bffbba
child 31153 6b31b143f18b
--- a/src/HOL/Library/Quickcheck.thy	Fri Apr 24 08:24:52 2009 +0200
+++ b/src/HOL/Library/Quickcheck.thy	Fri Apr 24 08:24:54 2009 +0200
@@ -74,8 +74,9 @@
   let
     val tys = (map snd o fst o strip_abs) t;
     val t' = mk_generator_expr thy t tys;
-    val f = Code_ML.eval (SOME target) ("Quickcheck.eval_ref", eval_ref) thy t' [];
-  in f #> Random_Engine.run #> (Option.map o map) (Code.postprocess_term thy) end;
+    val f = Code_ML.eval (SOME target) ("Quickcheck.eval_ref", eval_ref)
+      (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
+  in f #> Random_Engine.run end;
 
 end
 *}