mk_numeral
numSyntax.mk_numeral : Arbnum.num -> term
Convert ML bignum value to HOL numeral.
An invocation mk_numeral n, where n is an ML value of type
Arbnum.num returns the corrresponding HOL term.
Example
> Arbnum.fromString "1234";
val it = 1234: num
> numSyntax.mk_numeral it;
val it = “1234”: term
Failure
Never fails.