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\code_numeral"} $ @{term "j\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)