Maps a nonnegative integer to corresponding numeral term.
DESCRIPTION
The call mk_small_numeral n where n is a nonnegative OCaml machine integer
returns the HOL numeral representation of n.
FAILURE CONDITIONS
Fails if the argument is negative.
EXAMPLE
# mk_small_numeral 12;;
val it : term = `12`
COMMENTS
The similar function mk_numeral works from an unlimited precision integer,
OCaml type num. However, none of HOL's inference rules depend on the
behaviour of machine integers, so logical soundness is not an issue.