diff -r 650dcf624729 -r e50f1973cb0a src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Nov 24 12:35:13 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Nov 24 12:35:13 2014 +0100
@@ -804,36 +804,6 @@
          | Op2 (Less, T, Formula polar, u1, u2) =>
            formula_from_opt_atom polar bool_j0
                (to_r (Op2 (Less, T, Opt bool_atom_R, u1, u2)))
-         | Op2 (Subset, _, _, u1, u2) =>
-           let
-             val dom_T = pseudo_domain_type (type_of u1)
-             val R1 = rep_of u1
-             val R2 = rep_of u2
-             val (dom_R, ran_R) =
-               case min_rep R1 R2 of
-                 Func Rp => Rp
-               | R => (Atom (card_of_domain_from_rep 2 R,
-                             offset_of_type ofs dom_T),
-                       if is_opt_rep R then Opt bool_atom_R else Formula Neut)
-             val set_R = Func (dom_R, ran_R)
-           in
-             if not (is_opt_rep ran_R) then
-               to_set_bool_op kk_implies kk_subset u1 u2
-             else if polar = Neut then
-               raise NUT ("Nitpick_Kodkod.to_f (Subset)", [u])
-             else
-               let
-                 (* FIXME: merge with similar code below *)
-                 fun set_to_r widen u =
-                   if widen then
-                     kk_difference (full_rel_for_rep dom_R)
-                                   (kk_join (to_rep set_R u) false_atom)
-                   else
-                     kk_join (to_rep set_R u) true_atom
-                 val widen1 = (polar = Pos andalso is_opt_rep R1)
-                 val widen2 = (polar = Neg andalso is_opt_rep R2)
-               in kk_subset (set_to_r widen1 u1) (set_to_r widen2 u2) end
-           end
          | Op2 (DefEq, _, _, u1, u2) =>
            (case min_rep (rep_of u1) (rep_of u2) of
               Formula polar =>
@@ -1230,7 +1200,6 @@
                      (to_rep (Func (Struct [b_R, c_R], Formula Neut)) u2)
            | Opt (Atom (2, _)) =>
              let
-               (* FIXME: merge with similar code above *)
                fun must R1 R2 u =
                  kk_join (to_rep (Func (Struct [R1, R2], body_R)) u) true_atom
                fun may R1 R2 u =