--- a/src/HOL/Tools/quickcheck_generators.ML Thu Sep 16 08:18:34 2010 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Thu Sep 16 16:51:33 2010 +0200
@@ -392,16 +392,16 @@
in if Quickcheck.report ctxt then
let
val t' = mk_reporting_generator_expr thy t Ts;
- val compile = Code_Runtime.value (SOME target)
+ val compile = Code_Runtime.dynamic_value_strict
(Counterexample_Report.get, put_counterexample_report, "Quickcheck_Generators.put_counterexample_report")
- (fn proc => fn g => fn s => g s #>> (apfst o Option.map o map) proc) thy t' [];
+ thy (SOME target) (fn proc => fn g => fn s => g s #>> (apfst o Option.map o map) proc) t' [];
in compile #> Random_Engine.run end
else
let
val t' = mk_generator_expr thy t Ts;
- val compile = Code_Runtime.value (SOME target)
+ val compile = Code_Runtime.dynamic_value_strict
(Counterexample.get, put_counterexample, "Quickcheck_Generators.put_counterexample")
- (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
+ thy (SOME target) (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) t' [];
val dummy_report = ([], false)
in compile #> Random_Engine.run #> rpair dummy_report end
end;