changeset 59621 | 291934bac95e |
parent 59586 | ddf6deaadfe8 |
child 59996 | 4dca48557921 |
--- a/src/HOL/Tools/int_arith.ML Fri Mar 06 14:01:08 2015 +0100 +++ b/src/HOL/Tools/int_arith.ML Fri Mar 06 15:58:56 2015 +0100 @@ -82,7 +82,7 @@ fun number_of thy T n = if not (Sign.of_sort thy (T, @{sort numeral})) then raise CTERM ("number_of", []) - else Numeral.mk_cnumber (Thm.ctyp_of thy T) n; + else Numeral.mk_cnumber (Thm.global_ctyp_of thy T) n; val setup = Lin_Arith.add_inj_thms [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]