src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 41049 0edd245892ed
parent 41018 83f241623b86
child 41050 effbaa323cf0
     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 @@ -912,17 +912,6 @@
     1.4                  (MFun (bc_set_M, A Gen, MFun (ab_set_M, A Gen, ac_set_M)),
     1.5                   accum ||> add_annotation_atom_comp Neq [] (V x) (A New))
     1.6                end
     1.7 -            | @{const_name image} =>
     1.8 -              let
     1.9 -                val x = Unsynchronized.inc max_fresh
    1.10 -                val a_M = mtype_for (domain_type (domain_type T))
    1.11 -                val b_M = mtype_for (range_type (domain_type T))
    1.12 -              in
    1.13 -                (MFun (MFun (a_M, A Gen, b_M), A Gen,
    1.14 -                       MFun (MFun (a_M, V x, bool_M), A Gen,
    1.15 -                             MFun (b_M, V x, bool_M))),
    1.16 -                 accum ||> add_annotation_atom_comp Neq [] (V x) (A New))
    1.17 -              end
    1.18              | @{const_name finite} =>
    1.19                let
    1.20                  val M1 = mtype_for (domain_type (domain_type T))