1636 (hol_ctxt as {thy, ctxt, stds, whacks, total_consts, case_names, |
1636 (hol_ctxt as {thy, ctxt, stds, whacks, total_consts, case_names, |
1637 def_tables, ground_thm_table, ersatz_table, ...}) = |
1637 def_tables, ground_thm_table, ersatz_table, ...}) = |
1638 let |
1638 let |
1639 fun do_term depth Ts t = |
1639 fun do_term depth Ts t = |
1640 case t of |
1640 case t of |
1641 (t0 as Const (@{const_name Int.number_class.number_of}, |
1641 (t0 as Const (@{const_name Num.numeral_class.numeral}, |
1642 Type (@{type_name fun}, [_, ran_T]))) $ t1 => |
1642 Type (@{type_name fun}, [_, ran_T]))) $ t1 => |
1643 ((if is_number_type ctxt ran_T then |
1643 ((if is_number_type ctxt ran_T then |
1644 let |
1644 let |
1645 val j = t1 |> HOLogic.dest_numeral |
1645 val j = t1 |> HOLogic.dest_num |
1646 |> ran_T = nat_T ? Integer.max 0 |
1646 |> ran_T = nat_T ? Integer.max 0 |
1647 val s = numeral_prefix ^ signed_string_of_int j |
1647 val s = numeral_prefix ^ signed_string_of_int j |
1648 in |
1648 in |
1649 if is_integer_like_type ran_T then |
1649 if is_integer_like_type ran_T then |
1650 if is_standard_datatype thy stds ran_T then |
1650 if is_standard_datatype thy stds ran_T then |