# HG changeset patch
# User wenzelm
# Date 1302354023 -7200
# Node ID 1044726454437974b96d91f5aefc809b9ef50d6a
# Parent  941627f5477ad905f863c2c4a3faa5bbfaa44ccb
made SML/NJ happy;

diff -r 941627f5477a -r 104472645443 src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- 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 =