# HG changeset patch
# User blanchet
# Date 1258483647 -3600
# Node ID e82531ebf5f3639c07ea5996b418aaf68e749c2f
# Parent  a58893035742ccef92e03576d3927afa1cec1fe6
fixed bug in Nitpick's handling of "The" and "Eps" when the return type is a "bool"

diff -r a58893035742 -r e82531ebf5f3 src/HOL/Tools/Nitpick/HISTORY
--- a/src/HOL/Tools/Nitpick/HISTORY	Tue Nov 17 19:12:10 2009 +0100
+++ b/src/HOL/Tools/Nitpick/HISTORY	Tue Nov 17 19:47:27 2009 +0100
@@ -12,6 +12,8 @@
   * Added support for codatatype view of datatypes
   * Fixed soundness bugs related to sets and sets of sets
   * Fixed monotonicity check
+  * Fixed error when processing definitions that resulted in an exception
+  * Fixed error in Kodkod encoding of "The" and "Eps"
   * Fixed error in display of uncurried constants
   * Speeded up scope enumeration
 
diff -r a58893035742 -r e82531ebf5f3 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Nov 17 19:12:10 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Nov 17 19:47:27 2009 +0100
@@ -434,11 +434,11 @@
                          def_us
         val nondef_us = map (choose_reps_in_nut scope liberal rep_table false)
                             nondef_us
-(*
+(*###
+*)
         val _ = List.app (priority o string_for_nut ctxt)
                          (free_names @ sel_names @ nonsel_names @
                           core_u :: def_us @ nondef_us)
-*)
         val (free_rels, pool, rel_table) =
           rename_free_vars free_names initial_pool NameTable.empty
         val (sel_rels, pool, rel_table) =
diff -r a58893035742 -r e82531ebf5f3 src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Nov 17 19:12:10 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Nov 17 19:47:27 2009 +0100
@@ -1092,6 +1092,12 @@
                   else
                     kk_rel_eq r1 r2
                 end)
+         | Op2 (The, T, _, u1, u2) =>
+           to_f_with_polarity polar
+                              (Op2 (The, T, Opt (Atom (2, bool_j0)), u1, u2))
+         | Op2 (Eps, T, _, u1, u2) =>
+           to_f_with_polarity polar
+                              (Op2 (Eps, T, Opt (Atom (2, bool_j0)), u1, u2))
          | Op2 (Apply, T, _, u1, u2) =>
            (case (polar, rep_of u1) of
               (Neg, Func (R, Formula Neut)) => kk_subset (to_opt R u2) (to_r u1)
diff -r a58893035742 -r e82531ebf5f3 src/HOL/Tools/Nitpick/nitpick_nut.ML
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Nov 17 19:12:10 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Nov 17 19:47:27 2009 +0100
@@ -1158,8 +1158,10 @@
             let
               val u1' = sub u1
               val opt1 = is_opt_rep (rep_of u1')
+              val opt = (oper = Eps orelse opt1)
               val unopt_R = best_one_rep_for_type scope T |> optable_rep ofs T
-              val R = unopt_R |> (oper = Eps orelse opt1) ? opt_rep ofs T
+              val R = if is_boolean_type T then bool_rep polar opt
+                      else unopt_R |> opt ? opt_rep ofs T
               val u = Op2 (oper, T, R, u1', sub u2)
             in
               if is_precise_type datatypes T orelse not opt1 then