src/HOL/Tools/numeral_syntax.ML
changeset 11488 4ff900551340
parent 10891 890b117f6189
child 11701 3d51fbf81c17
     1.1 --- a/src/HOL/Tools/numeral_syntax.ML	Wed Aug 08 17:37:47 2001 +0200
     1.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Wed Aug 08 17:38:29 2001 +0200
     1.3 @@ -56,12 +56,12 @@
     1.4  
     1.5  (* translation of integer numeral tokens to and from bitstrings *)
     1.6  
     1.7 -fun numeral_tr (*"_Numeral"*) [t as Free (str, _)] =
     1.8 +fun numeral_tr (*"_Numeral"*) [t as Const (str, _)] =
     1.9        (Syntax.const "Numeral.number_of" $ HOLogic.mk_bin (Syntax.read_xnum str))
    1.10    | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
    1.11  
    1.12  fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =
    1.13 -      let val t' = Syntax.const "_Numeral" $ (Syntax.const "_xnum" $ Syntax.free (dest_bin_str t)) in
    1.14 +      let val t' = Syntax.const "_Numeral" $ Syntax.free (dest_bin_str t) in
    1.15          if not (! show_types) andalso can Term.dest_Type T then t'
    1.16          else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T
    1.17        end