be liberal about missing types;
authorwenzelm
Tue May 07 14:28:34 2002 +0200 (2002-05-07)
changeset 13110ca8cd110f769
parent 13109 39bcf279f518
child 13111 2d6782e71702
be liberal about missing types;
src/HOL/Tools/numeral_syntax.ML
     1.1 --- a/src/HOL/Tools/numeral_syntax.ML	Tue May 07 14:28:34 2002 +0200
     1.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Tue May 07 14:28:34 2002 +0200
     1.3 @@ -69,6 +69,9 @@
     1.4          if not (! show_types) andalso can Term.dest_Type T then t'
     1.5          else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T
     1.6        end
     1.7 +  | numeral_tr' _ (*"number_of"*) T (t :: ts) =
     1.8 +      if T = dummyT then Syntax.const "_Numeral" $ Syntax.free (dest_bin_str t)
     1.9 +      else raise Match
    1.10    | numeral_tr' _ (*"number_of"*) _ _ = raise Match;
    1.11  
    1.12