1.1 --- a/src/HOL/Tools/quickcheck_generators.ML Wed Sep 23 13:42:53 2009 +0200
1.2 +++ b/src/HOL/Tools/quickcheck_generators.ML Wed Sep 23 14:00:12 2009 +0200
1.3 @@ -76,7 +76,7 @@
1.4 val lhs = HOLogic.mk_random T size;
1.5 val rhs = HOLogic.mk_ST [((HOLogic.mk_random T' size, @{typ Random.seed}), SOME (v, Tm'))]
1.6 (HOLogic.mk_return Tm @{typ Random.seed}
1.7 - (mk_const "Code_Eval.valapp" [T', T]
1.8 + (mk_const "Code_Evaluation.valapp" [T', T]
1.9 $ HOLogic.mk_prod (t_constr, Abs ("u", @{typ unit}, HOLogic.reflect_term t_constr)) $ t_v))
1.10 @{typ Random.seed} (SOME Tm, @{typ Random.seed});
1.11 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));