diff -r 5c2f16eae066 -r e5a23ffb5524 src/HOL/Tools/Nitpick/nitpick_mono.ML --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Dec 06 13:33:09 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Dec 06 13:33:09 2010 +0100 @@ -790,10 +790,11 @@ fun do_all T (gamma, cset) = let val abs_M = mtype_for (domain_type (domain_type T)) + val x = Unsynchronized.inc max_fresh val body_M = mtype_for (body_type T) in - (MFun (MFun (abs_M, A Gen, body_M), A Gen, body_M), - (gamma, cset |> add_mtype_is_complete [] abs_M)) + (MFun (MFun (abs_M, V x, body_M), A Gen, body_M), + (gamma, cset |> add_mtype_is_complete [(x, (Plus, Tru))] abs_M)) end fun do_equals T (gamma, cset) = let