src/HOL/Tools/numeral_syntax.ML
changeset 19481 a6205c6203ea
parent 19381 6cd8abc7f15b
child 20067 26bac504ef90
     1.1 --- a/src/HOL/Tools/numeral_syntax.ML	Thu Apr 27 12:11:05 2006 +0200
     1.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Thu Apr 27 12:11:56 2006 +0200
     1.3 @@ -38,7 +38,7 @@
     1.4  (* translation of integer numeral tokens to and from bitstrings *)
     1.5  
     1.6  fun numeral_tr (*"_Numeral"*) [t as Const (str, _)] =
     1.7 -      (Syntax.const "Numeral.number_of" $ (HOLogic.mk_bin (valOf (IntInf.fromString str))))
     1.8 +      (Syntax.const "Numeral.number_of" $ (HOLogic.mk_binum (valOf (IntInf.fromString str))))
     1.9    | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
    1.10  
    1.11  fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =