# HG changeset patch
# User blanchet
# Date 1335357201 -7200
# Node ID 792634c6679e013b326bcd25f55075075e5c12e7
# Parent  0814fc93ab89c599c42b0ad8237bbd18c8733671
improve precision (noticed on SEV296^5.thy) -- the exception for "bool" used to be necessary because of a hack where "opt" meant two different things

diff -r 0814fc93ab89 -r 792634c6679e src/HOL/Tools/Nitpick/nitpick_nut.ML
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Wed Apr 25 14:33:21 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Wed Apr 25 14:33:21 2012 +0200
@@ -970,13 +970,8 @@
                val u1' = aux table' false Neut u1
                val u2' = aux table' false Neut u2
                val R =
-                 if is_opt_rep (rep_of u2') orelse
-                    (pseudo_range_type T = bool_T andalso
-                     not (is_Cst False (unrepify_nut_in_nut table false Neut
-                                                            u1 u2))) then
-                   opt_rep ofs T R
-                 else
-                   unopt_rep R
+                 if is_opt_rep (rep_of u2') then opt_rep ofs T R
+                 else unopt_rep R
              in s_op2 Lambda T R u1' u2' end
            | _ => raise NUT ("Nitpick_Nut.choose_reps_in_nut.aux", [u]))
         | Op2 (oper, T, _, u1, u2) =>