# HG changeset patch
# User blanchet
# Date 1280830592 -7200
# Node ID 5f2ea92319e07e28f14e18a5fbba140337e77ce5
# Parent  d74b66ec02ceafbdc4be9d21f7db86f9b42a020d
fix soundness bug w.r.t. "Suc" with "binary_ints"

diff -r d74b66ec02ce -r 5f2ea92319e0 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Aug 03 02:18:05 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Aug 03 12:16:32 2010 +0200
@@ -294,9 +294,10 @@
                    "\" could not be proved well-founded. Nitpick might need to \
                    \unroll it.")))
     val _ = if verbose then List.app print_wf (!wf_cache) else ()
+    val das_wort_formula = if falsify then "Negated conjecture" else "Formula"
     val _ =
       pprint_d (fn () => Pretty.chunks
-          (pretties_for_formulas ctxt "Preprocessed formula" [hd nondef_ts] @
+          (pretties_for_formulas ctxt das_wort_formula [hd nondef_ts] @
            pretties_for_formulas ctxt "Relevant definitional axiom" def_ts @
            pretties_for_formulas ctxt "Relevant nondefinitional axiom"
                                  (tl nondef_ts)))
diff -r d74b66ec02ce -r 5f2ea92319e0 src/HOL/Tools/Nitpick/nitpick_nut.ML
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Aug 03 02:18:05 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Aug 03 12:16:32 2010 +0200
@@ -746,8 +746,7 @@
   (not (is_fun_type (type_of u)) andalso not (is_opt_rep (rep_of u))) orelse
   case u of
     Cst (Num _, _, _) => true
-  | Cst (cst, T, _) =>
-    cst = Suc orelse (body_type T = nat_T andalso cst = Add)
+  | Cst (cst, T, _) => body_type T = nat_T andalso (cst = Suc orelse cst = Add)
   | Op2 (Apply, _, _, u1, u2) => forall is_constructive [u1, u2]
   | Op3 (If, _, _, u1, u2, u3) =>
     not (is_opt_rep (rep_of u1)) andalso forall is_constructive [u2, u3]