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