src/HOL/Tools/numeral_syntax.ML
changeset 7429 8f284fbb8728
parent 7078 4e64b2bd10ce
child 7550 060f9954f73d
equal deleted inserted replaced
7428:80838c2af97b 7429:8f284fbb8728
    89         (bin_of_string str handle ERROR => raise TERM ("numeral_tr", [t])))
    89         (bin_of_string str handle ERROR => raise TERM ("numeral_tr", [t])))
    90   | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
    90   | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
    91 
    91 
    92 fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =
    92 fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =
    93       let val t' = Syntax.const "_Numeral" $ (Syntax.const "_xnum" $ Syntax.free (dest_bin_str t)) in
    93       let val t' = Syntax.const "_Numeral" $ (Syntax.const "_xnum" $ Syntax.free (dest_bin_str t)) in
    94         if can Term.dest_Type T then t'
    94         if not (! show_types) andalso can Term.dest_Type T then t'
    95         else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T
    95         else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T
    96       end
    96       end
    97   | numeral_tr' _ (*"number_of"*) _ _ = raise Match;
    97   | numeral_tr' _ (*"number_of"*) _ _ = raise Match;
    98 
    98 
    99 
    99