src/HOL/Tools/numeral_syntax.ML
changeset 13110 ca8cd110f769
parent 11701 3d51fbf81c17
child 13491 ddf6ae639f21
equal deleted inserted replaced
13109:39bcf279f518 13110:ca8cd110f769
    67 fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =
    67 fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =
    68       let val t' = Syntax.const "_Numeral" $ Syntax.free (dest_bin_str t) in
    68       let val t' = Syntax.const "_Numeral" $ Syntax.free (dest_bin_str t) in
    69         if not (! show_types) andalso can Term.dest_Type T then t'
    69         if not (! show_types) andalso can Term.dest_Type T then t'
    70         else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T
    70         else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T
    71       end
    71       end
       
    72   | numeral_tr' _ (*"number_of"*) T (t :: ts) =
       
    73       if T = dummyT then Syntax.const "_Numeral" $ Syntax.free (dest_bin_str t)
       
    74       else raise Match
    72   | numeral_tr' _ (*"number_of"*) _ _ = raise Match;
    75   | numeral_tr' _ (*"number_of"*) _ _ = raise Match;
    73 
    76 
    74 
    77 
    75 (* theory setup *)
    78 (* theory setup *)
    76 
    79