src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 41012 e5a23ffb5524
parent 41011 5c2f16eae066
child 41013 117345744f44
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
     1.3 @@ -790,10 +790,11 @@
     1.4      fun do_all T (gamma, cset) =
     1.5        let
     1.6          val abs_M = mtype_for (domain_type (domain_type T))
     1.7 +        val x = Unsynchronized.inc max_fresh
     1.8          val body_M = mtype_for (body_type T)
     1.9        in
    1.10 -        (MFun (MFun (abs_M, A Gen, body_M), A Gen, body_M),
    1.11 -         (gamma, cset |> add_mtype_is_complete [] abs_M))
    1.12 +        (MFun (MFun (abs_M, V x, body_M), A Gen, body_M),
    1.13 +         (gamma, cset |> add_mtype_is_complete [(x, (Plus, Tru))] abs_M))
    1.14        end
    1.15      fun do_equals T (gamma, cset) =
    1.16        let