diff -r 1e5f382c48cc -r 5c2f16eae066 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
@@ -246,7 +246,7 @@
                 $ (Const (@{const_name unknown}, ran_T)) $ (t0 $ t1 $ t2 $ t3)))
   | fin_fun_body _ _ _ = NONE
 
-(* ### FIXME: make sure wellformed! *)
+(* ### FIXME: make sure well-annotated! *)
 
 fun fresh_mfun_for_fun_type (mdata as {max_fresh, ...} : mdata) all_minus
                             T1 T2 =
@@ -787,8 +787,6 @@
         <= length ts
       | _ => true
     val mtype_for = fresh_mtype_for_type mdata false
-    fun plus_set_mtype_for_dom M =
-      MFun (M, A (if exists_alpha_sub_mtype M then Fls else Gen), bool_M)
     fun do_all T (gamma, cset) =
       let
         val abs_M = mtype_for (domain_type (domain_type T))
@@ -891,7 +889,10 @@
                   MFun (mtype_for (domain_type T), V x, bool_M)
                 val ab_set_M = domain_type T |> mtype_for_set
                 val ba_set_M = range_type T |> mtype_for_set
-              in (MFun (ab_set_M, A Gen, ba_set_M), accum) end
+              in
+                (MFun (ab_set_M, A Gen, ba_set_M),
+                 accum ||> add_annotation_atom_comp Neq [] (V x) (A New))
+              end
             | @{const_name trancl} => do_fragile_set_operation T accum
             | @{const_name rel_comp} =>
               let
@@ -903,21 +904,24 @@
                 val ac_set_M = nth_range_type 2 T |> mtype_for_set
               in
                 (MFun (bc_set_M, A Gen, MFun (ab_set_M, A Gen, ac_set_M)),
-                 accum)
+                 accum ||> add_annotation_atom_comp Neq [] (V x) (A New))
               end
             | @{const_name image} =>
               let
+                val x = Unsynchronized.inc max_fresh
                 val a_M = mtype_for (domain_type (domain_type T))
                 val b_M = mtype_for (range_type (domain_type T))
               in
                 (MFun (MFun (a_M, A Gen, b_M), A Gen,
-                       MFun (plus_set_mtype_for_dom a_M, A Gen,
-                             plus_set_mtype_for_dom b_M)), accum)
+                       MFun (MFun (a_M, V x, bool_M), A Gen,
+                             MFun (b_M, V x, bool_M))),
+                 accum ||> add_annotation_atom_comp Neq [] (V x) (A New))
               end
             | @{const_name finite} =>
-              let val M1 = mtype_for (domain_type (domain_type T)) in
-                (MFun (plus_set_mtype_for_dom M1, A Gen, bool_M), accum)
-              end
+              let
+                val M1 = mtype_for (domain_type (domain_type T))
+                val a = if exists_alpha_sub_mtype M1 then Fls else Gen
+              in (MFun (MFun (M1, A a, bool_M), A Gen, bool_M), accum) end
             | @{const_name Sigma} =>
               let
                 val x = Unsynchronized.inc max_fresh
@@ -932,7 +936,7 @@
                 val ab_set_M = mtype_for_set (nth_range_type 2 T)
               in
                 (MFun (a_set_M, A Gen, MFun (a_to_b_set_M, A Gen, ab_set_M)),
-                 accum)
+                 accum ||> add_annotation_atom_comp Neq [] (V x) (A New))
               end
             | _ =>
               if s = @{const_name safe_The} then