src/HOL/Tools/int_arith.ML
changeset 47108 2a1953f0d20d
parent 43595 7ae4a23b5be6
child 47209 4893907fe872
     1.1 --- a/src/HOL/Tools/int_arith.ML	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/Tools/int_arith.ML	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -78,7 +78,7 @@
     1.4    proc = sproc, identifier = []}
     1.5  
     1.6  fun number_of thy T n =
     1.7 -  if not (Sign.of_sort thy (T, @{sort number}))
     1.8 +  if not (Sign.of_sort thy (T, @{sort numeral}))
     1.9    then raise CTERM ("number_of", [])
    1.10    else Numeral.mk_cnumber (Thm.ctyp_of thy T) n;
    1.11