1.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Thu Nov 12 14:47:54 2009 +0100
1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Nov 17 19:47:27 2009 +0100
1.3 @@ -1158,8 +1158,10 @@
1.4 let
1.5 val u1' = sub u1
1.6 val opt1 = is_opt_rep (rep_of u1')
1.7 + val opt = (oper = Eps orelse opt1)
1.8 val unopt_R = best_one_rep_for_type scope T |> optable_rep ofs T
1.9 - val R = unopt_R |> (oper = Eps orelse opt1) ? opt_rep ofs T
1.10 + val R = if is_boolean_type T then bool_rep polar opt
1.11 + else unopt_R |> opt ? opt_rep ofs T
1.12 val u = Op2 (oper, T, R, u1', sub u2)
1.13 in
1.14 if is_precise_type datatypes T orelse not opt1 then