
diff -r 251a34663242 -r 71f163982a21 src/HOL/ex/Quickcheck_Generators.thy
--- a/src/HOL/ex/Quickcheck_Generators.thy	Sun May 24 15:02:21 2009 +0200
+++ b/src/HOL/ex/Quickcheck_Generators.thy	Sun May 24 15:02:22 2009 +0200
@@ -79,10 +79,11 @@
         else raise TYP
           ("Will not generate random elements for type(s) " ^ quote (hd tycos));
       fun dtyp tyco = ((this_ty, true), random' $ @{term "i\<Colon>code_numeral"} $ @{term "j\<Colon>code_numeral"});
-      fun rtyp tyco tys = raise REC
+      fun rtyp (tyco, Ts) _ = raise REC
         ("Will not generate random elements for mutual recursive type " ^ quote (hd tycos));
       val rhss = DatatypePackage.construction_interpretation thy
             { atom = atom, dtyp = dtyp, rtyp = rtyp } vs tycos
+        |> fst
         |> (map o apsnd o map) (mk_cons thy this_ty) 
         |> (map o apsnd) (List.partition fst)
         |> map (mk_clauses thy this_ty)




