# HG changeset patch
# User blanchet
# Date 1258494660 -3600
# Node ID 6c6ce0757bfef2256782d7d954d2522c10392639
# Parent  4c414d0835ab3128a0b0300c95e24d9874999660# Parent  daf236998f8233ff648dc1e5a1bb0f6b6b1b7607
merged

diff -r 4c414d0835ab -r 6c6ce0757bfe src/HOL/Nitpick_Examples/ROOT.ML
--- a/src/HOL/Nitpick_Examples/ROOT.ML	Tue Nov 17 18:52:30 2009 +0100
+++ b/src/HOL/Nitpick_Examples/ROOT.ML	Tue Nov 17 22:51:00 2009 +0100
@@ -5,7 +5,6 @@
 Nitpick examples.
 *)
 
-Toplevel.debug := true;
 if getenv "KODKODI" = "" then
   ()
 else
diff -r 4c414d0835ab -r 6c6ce0757bfe src/HOL/Tools/Nitpick/HISTORY
--- a/src/HOL/Tools/Nitpick/HISTORY	Tue Nov 17 18:52:30 2009 +0100
+++ b/src/HOL/Tools/Nitpick/HISTORY	Tue Nov 17 22:51:00 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 4c414d0835ab -r 6c6ce0757bfe src/HOL/Tools/Nitpick/nitpick.ML
diff -r 4c414d0835ab -r 6c6ce0757bfe src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Nov 17 18:52:30 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Nov 17 22:51:00 2009 +0100
@@ -1109,13 +1109,13 @@
     |> map_filter (try (Refute.specialize_type thy x))
     |> filter (equal (Const x) o term_under_def)
 
-(* term -> term *)
+(* theory -> term -> term option *)
 fun normalized_rhs_of thy t =
   let
-    (* term -> term *)
-    fun aux (v as Var _) t = lambda v t
-      | aux (c as Const (@{const_name TYPE}, T)) t = lambda c t
-      | aux _ _ = raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
+    (* term option -> term option *)
+    fun aux (v as Var _) (SOME t) = SOME (lambda v t)
+      | aux (c as Const (@{const_name TYPE}, T)) (SOME t) = SOME (lambda c t)
+      | aux _ _ = NONE
     val (lhs, rhs) =
       case t of
         Const (@{const_name "=="}, _) $ t1 $ t2 => (t1, t2)
@@ -1123,7 +1123,7 @@
         (t1, t2)
       | _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
     val args = strip_comb lhs |> snd
-  in fold_rev aux args rhs end
+  in fold_rev aux args (SOME rhs) end
 
 (* theory -> const_table -> styp -> term option *)
 fun def_of_const thy table (x as (s, _)) =
@@ -1131,7 +1131,7 @@
     NONE
   else
     x |> def_props_for_const thy false table |> List.last
-      |> normalized_rhs_of thy |> prefix_abs_vars s |> SOME
+      |> normalized_rhs_of thy |> Option.map (prefix_abs_vars s)
     handle List.Empty => NONE
 
 datatype fixpoint_kind = Lfp | Gfp | NoFp
diff -r 4c414d0835ab -r 6c6ce0757bfe src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Nov 17 18:52:30 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Nov 17 22:51:00 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 4c414d0835ab -r 6c6ce0757bfe src/HOL/Tools/Nitpick/nitpick_nut.ML
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Nov 17 18:52:30 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Nov 17 22:51:00 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