--- a/src/HOL/Tools/quickcheck_generators.ML Sun Jun 21 19:19:52 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Sun Jun 21 21:37:24 2009 +0200
@@ -362,16 +362,20 @@
val algebra = Sign.classes_of thy;
val (descr, raw_vs, tycos, (names, auxnames), raw_TUs) =
Datatype.the_datatype_descr thy raw_tycos;
+ val typrep_vs = (map o apsnd)
+ (curry (Sorts.inter_sort algebra) @{sort typerep}) raw_vs;
val random_insts = (map (rpair @{sort random}) o flat o maps snd o maps snd)
- (DatatypeAux.interpret_construction descr raw_vs { atyp = single, dtyp = (K o K o K) [] });
+ (DatatypeAux.interpret_construction descr typrep_vs
+ { atyp = single, dtyp = (K o K o K) [] });
val term_of_insts = (map (rpair @{sort term_of}) o flat o maps snd o maps snd)
- (DatatypeAux.interpret_construction descr raw_vs { atyp = K [], dtyp = K o K });
+ (DatatypeAux.interpret_construction descr typrep_vs
+ { atyp = K [], dtyp = K o K });
val has_inst = exists (fn tyco =>
can (Sorts.mg_domain algebra tyco) @{sort random}) tycos;
in if has_inst then thy
- else case perhaps_constrain thy (random_insts @ term_of_insts) raw_vs
+ else case perhaps_constrain thy (random_insts @ term_of_insts) typrep_vs
of SOME constrain => mk_random_datatype config descr
- (map constrain raw_vs) tycos (names, auxnames)
+ (map constrain typrep_vs) tycos (names, auxnames)
((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
| NONE => thy
end;