src/HOL/Tools/int_arith.ML

--- 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]