changeset 19481 | a6205c6203ea |
parent 19277 | f7602e74d948 |
child 20194 | c9dbce9a23a1 |
--- a/src/HOL/Integ/cooper_dec.ML Thu Apr 27 12:11:05 2006 +0200 +++ b/src/HOL/Integ/cooper_dec.ML Thu Apr 27 12:11:56 2006 +0200 @@ -80,7 +80,7 @@ fun mk_numeral 0 = Const("0",HOLogic.intT) |mk_numeral 1 = Const("1",HOLogic.intT) - |mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_bin n); + |mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_binum n); (*Transform an Term to an natural number*)