src/HOL/Tools/Nitpick/nitpick_nut.ML
changeset 33744 e82531ebf5f3
parent 33631 d3af5b21cbaf
child 33853 348c3ea03e58
     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