changeset 54294 | 98826791a588 |
parent 53815 | e8aa538e959e |
child 54489 | 03ff4d1e6784 |
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sun Nov 10 10:02:34 2013 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sun Nov 10 10:02:34 2013 +0100 @@ -1648,8 +1648,7 @@ fun do_numeral depth Ts mult T t0 t1 = (if is_number_type ctxt T then let - val j = mult * (HOLogic.dest_num t1) - |> T = nat_T ? Integer.max 0 + val j = mult * HOLogic.dest_num t1 in if j = 1 then raise SAME ()