--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Sat Apr 09 13:10:20 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Sat Apr 09 15:00:23 2011 +0200
@@ -247,9 +247,9 @@
(** instantiating generator classes **)
-val contains_recursive_type_under_function_types =
+fun contains_recursive_type_under_function_types xs =
exists (fn (_, (_, _, cs)) => cs |> exists (snd #> exists (fn dT =>
- (case Datatype_Aux.strip_dtyp dT of (_ :: _, Datatype.DtRec _) => true | _ => false))))
+ (case Datatype_Aux.strip_dtyp dT of (_ :: _, Datatype.DtRec _) => true | _ => false)))) xs
fun instantiate_datatype (name, constprfx, sort, mk_equations, mk_T, argnames)
config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =