src/HOL/Tools/numeral_syntax.ML
changeset 15965 f422f8283491
parent 15620 8ccdc8bc66a2
child 16365 838c65dad23a
     1.1 --- a/src/HOL/Tools/numeral_syntax.ML	Mon May 16 09:35:05 2005 +0200
     1.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Mon May 16 10:29:15 2005 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4        (case rev rev_digs of
     1.5          ~1 :: bs => ("-", prefix_len (equal 1) bs)
     1.6        | bs => ("", prefix_len (equal 0) bs));
     1.7 -    val i = HOLogic.intinf_of rev_digs;
     1.8 +    val i = HOLogic.int_of rev_digs;
     1.9      val num = IntInf.toString (IntInf.abs i);
    1.10    in
    1.11      if i = IntInf.fromInt 0 orelse i = IntInf.fromInt 1 then raise Match
    1.12 @@ -38,7 +38,7 @@
    1.13  (* translation of integer numeral tokens to and from bitstrings *)
    1.14  
    1.15  fun numeral_tr (*"_Numeral"*) [t as Const (str, _)] =
    1.16 -      (Syntax.const "Numeral.number_of" $ (HOLogic.mk_bin_from_intinf (valOf (IntInf.fromString str))))
    1.17 +      (Syntax.const "Numeral.number_of" $ (HOLogic.mk_bin (valOf (IntInf.fromString str))))
    1.18    | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
    1.19  
    1.20  fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =