equal
deleted
inserted
replaced
248 val t = fold_rev mk_bindclause bounds (return $ check); |
248 val t = fold_rev mk_bindclause bounds (return $ check); |
249 in Abs ("n", @{typ index}, t) end; |
249 in Abs ("n", @{typ index}, t) end; |
250 |
250 |
251 fun compile_generator_expr thy prop tys = |
251 fun compile_generator_expr thy prop tys = |
252 let |
252 let |
253 val f = CodeTarget.eval_term ("Quickcheck.eval_ref", eval_ref) thy |
253 val f = Code_ML.eval_term ("Quickcheck.eval_ref", eval_ref) thy |
254 (mk_generator_expr thy prop tys) []; |
254 (mk_generator_expr thy prop tys) []; |
255 in f #> Random_Engine.run #> (Option.map o map) (Code.postprocess_term thy) end; |
255 in f #> Random_Engine.run #> (Option.map o map) (Code.postprocess_term thy) end; |
256 |
256 |
257 fun VALUE prop tys thy = |
257 fun VALUE prop tys thy = |
258 let |
258 let |