author | haftmann |
Sun, 10 Nov 2013 10:02:34 +0100 | |
changeset 54294 | 98826791a588 |
parent 54293 | cd896760fa0f |
child 54295 | 45a5523d4a63 |
--- 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 ()