1.1 --- a/src/HOL/Tools/Nitpick/HISTORY	Tue Nov 24 12:29:08 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/HISTORY	Tue Nov 24 13:22:18 2009 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4      the formula to falsify
     1.5    * Added support for codatatype view of datatypes
     1.6    * Fixed soundness bugs related to sets, sets of sets, (co)inductive
     1.7 -    predicates, typedefs, and "finite"
     1.8 +    predicates, typedefs, "finite", and negative literals
     1.9    * Fixed monotonicity check
    1.10    * Fixed error when processing definitions
    1.11    * Fixed error in "star_linear_preds" optimization

     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Nov 24 12:29:08 2009 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Nov 24 13:22:18 2009 +0100
     2.3 @@ -1440,7 +1440,7 @@
     2.4          ((if is_number_type thy ran_T then
     2.5              let
     2.6                val j = t1 |> HOLogic.dest_numeral
     2.7 -                         |> ran_T <> int_T ? curry Int.max 0
     2.8 +                         |> ran_T = nat_T ? Integer.max 0
     2.9                val s = numeral_prefix ^ signed_string_of_int j
    2.10              in
    2.11                if is_integer_type ran_T then
    2.12 @@ -1656,7 +1656,7 @@
    2.13         let
    2.14           val binders_T = HOLogic.mk_tupleT (binder_types T)
    2.15           val rel_T = HOLogic.mk_prodT (binders_T, binders_T) --> bool_T
    2.16 -         val j = List.foldl Int.max 0 (map maxidx_of_term intro_ts) + 1
    2.17 +         val j = fold Integer.max (map maxidx_of_term intro_ts) 0 + 1
    2.18           val rel = (("R", j), rel_T)
    2.19           val prop = Const (@{const_name wf}, rel_T --> bool_T) $ Var rel ::
    2.20                      map (wf_constraint_for_triple rel) triples
    2.21 @@ -2922,7 +2922,7 @@
    2.22    let
    2.23      val (bounds1, bounds2) = pairself (map Var o special_bounds) (ts1, ts2)
    2.24      val Ts = binder_types T
    2.25 -    val max_j = fold (fold (curry Int.max)) [js1, js2] ~1
    2.26 +    val max_j = fold (fold Integer.max) [js1, js2] ~1
    2.27      val (eqs, (args1, args2)) =
    2.28        fold (fn j => case pairself (fn ps => AList.lookup (op =) ps j)
    2.29                                    (js1 ~~ ts1, js2 ~~ ts2) of