src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 41050 effbaa323cf0
parent 41049 0edd245892ed
child 41052 3db267a01c1d
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Dec 07 11:56:01 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Dec 07 11:56:01 2010 +0100
     1.3 @@ -917,20 +917,17 @@
     1.4                  val M1 = mtype_for (domain_type (domain_type T))
     1.5                  val a = if exists_alpha_sub_mtype M1 then Fls else Gen
     1.6                in (MFun (MFun (M1, A a, bool_M), A Gen, bool_M), accum) end
     1.7 -            | @{const_name Sigma} =>
     1.8 +            | @{const_name prod} =>
     1.9                let
    1.10                  val x = Unsynchronized.inc max_fresh
    1.11                  fun mtype_for_set T =
    1.12                    MFun (mtype_for (domain_type T), V x, bool_M)
    1.13 -                val a_set_T = domain_type T
    1.14 -                val a_M = mtype_for (domain_type a_set_T)
    1.15 +                val a_set_M = mtype_for_set (domain_type T)
    1.16                  val b_set_M =
    1.17                    mtype_for_set (range_type (domain_type (range_type T)))
    1.18 -                val a_set_M = mtype_for_set a_set_T
    1.19 -                val a_to_b_set_M = MFun (a_M, A Gen, b_set_M)
    1.20                  val ab_set_M = mtype_for_set (nth_range_type 2 T)
    1.21                in
    1.22 -                (MFun (a_set_M, A Gen, MFun (a_to_b_set_M, A Gen, ab_set_M)),
    1.23 +                (MFun (a_set_M, A Gen, MFun (b_set_M, A Gen, ab_set_M)),
    1.24                   accum ||> add_annotation_atom_comp Neq [] (V x) (A New))
    1.25                end
    1.26              | _ =>