1.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Wed Feb 17 11:20:09 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Wed Feb 17 12:14:08 2010 +0100
     1.3 @@ -892,7 +892,7 @@
     1.4  (* scope -> bool -> rep NameTable.table -> bool -> nut -> nut *)
     1.5  fun choose_reps_in_nut (scope as {hol_ctxt as {thy, ctxt, ...}, card_assigns,
     1.6                                    bits, datatypes, ofs, ...})
     1.7 -                       liberal table def =
     1.8 +                       unsound table def =
     1.9    let
    1.10      val bool_atom_R = Atom (2, offset_of_type ofs bool_T)
    1.11      (* polarity -> bool -> rep *)
    1.12 @@ -1036,7 +1036,7 @@
    1.13                if is_constructive u then s_op2 Eq T (Formula Neut) u1' u2'
    1.14                else opt_opt_case ()
    1.15            in
    1.16 -            if liberal orelse polar = Neg orelse
    1.17 +            if unsound orelse polar = Neg orelse
    1.18                 is_concrete_type datatypes (type_of u1) then
    1.19                case (is_opt_rep (rep_of u1'), is_opt_rep (rep_of u2')) of
    1.20                  (true, true) => opt_opt_case ()
    1.21 @@ -1138,7 +1138,7 @@
    1.22                else
    1.23                  let val quant_u = s_op2 oper T (Formula polar) u1' u2' in
    1.24                    if def orelse
    1.25 -                     (liberal andalso (polar = Pos) = (oper = All)) orelse
    1.26 +                     (unsound andalso (polar = Pos) = (oper = All)) orelse
    1.27                       is_complete_type datatypes (type_of u1) then
    1.28                      quant_u
    1.29                    else