| changeset 51126 | df86080de4cb |
| parent 47108 | 2a1953f0d20d |
| child 51143 | 0a2371e7ced3 |
--- a/src/HOL/Tools/hologic.ML Thu Feb 14 17:58:28 2013 +0100 +++ b/src/HOL/Tools/hologic.ML Thu Feb 14 15:27:10 2013 +0100 @@ -686,7 +686,7 @@ val random_seedT = mk_prodT (code_numeralT, code_numeralT); -fun mk_random T t = Const ("Quickcheck.random_class.random", code_numeralT +fun mk_random T t = Const ("Quickcheck_Random.random_class.random", code_numeralT --> random_seedT --> mk_prodT (mk_prodT (T, unitT --> termT), random_seedT)) $ t; end;