--- a/src/HOL/Tools/Quickcheck/random_generators.ML Wed Jun 08 22:16:21 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Thu Jun 09 20:22:22 2011 +0200
@@ -214,7 +214,7 @@
val tTs = (map o apsnd) termifyT simple_tTs;
val is_rec = exists is_some ks;
val k = fold (fn NONE => I | SOME k => Integer.max k) ks 0;
- val vs = Name.names Name.context "x" (map snd simple_tTs);
+ val vs = Name.invent_names Name.context "x" (map snd simple_tTs);
val tc = HOLogic.mk_return T @{typ Random.seed}
(HOLogic.mk_valtermify_app c vs simpleT);
val t = HOLogic.mk_ST