# HG changeset patch
# User blanchet
# Date 1368280824 -7200
# Node ID a5265222d6e6c18c7b786fcf44b9cfd67fd77985
# Parent  bcd6898ac613a9b214d409dbf98c4f02979d129e
fixed bug introduced when reintroducing set constructor, and visible when applying <= to 2- or more-ary relations, e.g. "(R::'a=>'a=>bool) <= R"

diff -r bcd6898ac613 -r a5265222d6e6 src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Fri May 10 19:41:23 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Sat May 11 16:00:24 2013 +0200
@@ -1379,9 +1379,11 @@
       in
         case min_R of
           Vect (k, Atom _) => kk_vect_set_bool_op connective k r1 r2
-        | Func (_, Formula Neut) => set_oper r1 r2
-        | Func (_, Atom _) => set_oper (kk_join r1 true_atom)
-                                       (kk_join r2 true_atom)
+        | Func (_, R') =>
+          (case body_rep R' of
+             Formula Neut => set_oper r1 r2
+           | Atom _ => set_oper (kk_join r1 true_atom) (kk_join r2 true_atom)
+           | _ => raise REP ("Nitpick_Kodkod.to_set_bool_op", [min_R]))
         | _ => raise REP ("Nitpick_Kodkod.to_set_bool_op", [min_R])
       end
     and to_bit_word_unary_op T R oper =