src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 47108 2a1953f0d20d
parent 46819 9b38f8527510
child 47109 db5026631799
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -1638,11 +1638,11 @@
     1.4    let
     1.5      fun do_term depth Ts t =
     1.6        case t of
     1.7 -        (t0 as Const (@{const_name Int.number_class.number_of},
     1.8 +        (t0 as Const (@{const_name Num.numeral_class.numeral},
     1.9                        Type (@{type_name fun}, [_, ran_T]))) $ t1 =>
    1.10          ((if is_number_type ctxt ran_T then
    1.11              let
    1.12 -              val j = t1 |> HOLogic.dest_numeral
    1.13 +              val j = t1 |> HOLogic.dest_num
    1.14                           |> ran_T = nat_T ? Integer.max 0
    1.15                val s = numeral_prefix ^ signed_string_of_int j
    1.16              in