# HG changeset patch
# User haftmann
# Date 1245613044 -7200
# Node ID dc3c2d52b642a16269526f3fbeaa6b622da20f48
# Parent  ce6c75e7ab200df33ddcb720cfa6ffaccb6ec549
more precise computation of sort constraints

diff -r ce6c75e7ab20 -r dc3c2d52b642 src/HOL/Tools/quickcheck_generators.ML
--- 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;