# 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]