| changeset 19481 | a6205c6203ea |
| parent 19297 | 8f6e097d7b23 |
| child 19823 | 9e4573eaacb3 |
--- a/src/HOL/arith_data.ML Thu Apr 27 12:11:05 2006 +0200 +++ b/src/HOL/arith_data.ML Thu Apr 27 12:11:56 2006 +0200 @@ -367,7 +367,7 @@ let val {discrete, inj_consts, ...} = ArithTheoryData.get sg in decomp2 (sg,discrete,inj_consts) end -fun number_of(n,T) = HOLogic.number_of_const T $ (HOLogic.mk_bin n) +fun number_of(n,T) = HOLogic.number_of_const T $ (HOLogic.mk_binum n) end;