# HG changeset patch
# User blanchet
# Date 1262863475 -3600
# Node ID cf455b5880e15f1e4292f170b22fe98b1c2eb562
# Parent  16496e04ca462f9e1bc9c3e6ed3215643f10d741
reduced arity of Nitpick selectors associated with sets by 1, by using "Formula" instead of "Atom 2"

diff -r 16496e04ca46 -r cf455b5880e1 src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Jan 07 08:45:55 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Jan 07 12:24:35 2010 +0100
@@ -1629,7 +1629,7 @@
                                (KK.Atom j0) KK.None)
          | _ => raise NUT ("Nitpick_Kodkod.to_r (Tuple)", [u]))
       | Construct ([u'], _, _, []) => to_r u'
-      | Construct (_ :: sel_us, T, R, arg_us) =>
+      | Construct (discr_u :: sel_us, T, R, arg_us) =>
         let
           val set_rs =
             map2 (fn sel_u => fn arg_u =>
@@ -1642,8 +1642,7 @@
                          kk_n_fold_join kk true R2 R1 arg_r
                               (kk_project sel_r (flip_nums (arity_of_rep R2)))
                        else
-                         kk_comprehension
-                             (decls_for_atom_schema ~1 (atom_schema_of_rep R1))
+                         kk_comprehension [KK.DeclOne ((1, ~1), to_r discr_u)]
                              (kk_rel_eq (kk_join (KK.Var (1, ~1)) sel_r) arg_r)
                      end) sel_us arg_us
         in fold1 kk_intersect set_rs end
diff -r 16496e04ca46 -r cf455b5880e1 src/HOL/Tools/Nitpick/nitpick_nut.ML
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Thu Jan 07 08:45:55 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Thu Jan 07 12:24:35 2010 +0100
@@ -746,7 +746,9 @@
                                       (vs, table) =
   let
     val (s', T') = boxed_nth_sel_for_constr ext_ctxt x n
-    val R' = if n = ~1 orelse is_word_type (body_type T) then
+    val R' = if n = ~1 orelse is_word_type (body_type T)
+                orelse (is_fun_type (range_type T')
+                        andalso is_boolean_type (body_type T')) then
                best_non_opt_set_rep_for_type scope T'
              else
                best_opt_set_rep_for_type scope T' |> unopt_rep