changeset 62342 | 1cf129590be8 |
parent 61858 | 3f494c048142 |
child 62500 | ff99681b3fd8 |
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Feb 17 21:08:18 2016 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Feb 17 21:51:55 2016 +0100 @@ -1672,7 +1672,7 @@ fun do_numeral depth Ts mult T some_t0 t1 t2 = (if is_number_type ctxt T then let - val j = mult * HOLogic.dest_num t2 + val j = mult * HOLogic.dest_numeral t2 in if j = 1 then raise SAME ()