src/HOL/Num.thy
changeset 59621 291934bac95e
parent 58889 5b7a9633cfa8
child 59867 58043346ca64
     1.1 --- a/src/HOL/Num.thy	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/HOL/Num.thy	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -1198,7 +1198,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  in
    1.10    K (
    1.11      Lin_Arith.add_simps (@{thms arith_simps} @ @{thms more_arith_simps}