src/HOL/Tools/quickcheck_generators.ML
changeset 32657 5f13912245ff
parent 32378 89b19ab3b35c
child 32740 9dd0a2f83429
     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));