dropped obsolete check: dest_num always yields positive number
authorhaftmann
Sun Nov 10 10:02:34 2013 +0100 (2013-11-10)
changeset 5429498826791a588
parent 54293 cd896760fa0f
child 54295 45a5523d4a63
dropped obsolete check: dest_num always yields positive number
src/HOL/Tools/Nitpick/nitpick_hol.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Nov 10 10:02:34 2013 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Nov 10 10:02:34 2013 +0100
     1.3 @@ -1648,8 +1648,7 @@
     1.4      fun do_numeral depth Ts mult T t0 t1 =
     1.5        (if is_number_type ctxt T then
     1.6           let
     1.7 -           val j = mult * (HOLogic.dest_num t1)
     1.8 -                   |> T = nat_T ? Integer.max 0
     1.9 +           val j = mult * HOLogic.dest_num t1
    1.10           in
    1.11             if j = 1 then
    1.12               raise SAME ()