| changeset 19481 | a6205c6203ea |
| parent 19277 | f7602e74d948 |
| child 19617 | 7cb4b67d4b97 |
--- a/src/HOL/Integ/int_arith1.ML Thu Apr 27 12:11:05 2006 +0200 +++ b/src/HOL/Integ/int_arith1.ML Thu Apr 27 12:11:56 2006 +0200 @@ -182,7 +182,7 @@ (** Utilities **) -fun mk_numeral T n = HOLogic.number_of_const T $ HOLogic.mk_bin n; +fun mk_numeral T n = HOLogic.number_of_const T $ HOLogic.mk_binum n; (*Decodes a binary INTEGER*) fun dest_numeral (Const("0", _)) = 0