# HG changeset patch # User wenzelm # Date 1020774514 -7200 # Node ID ca8cd110f769e9df8fabfaccf9703be5a205dc5f # Parent 39bcf279f518b3d307d31148cdaecc3b37a18899 be liberal about missing types; diff -r 39bcf279f518 -r ca8cd110f769 src/HOL/Tools/numeral_syntax.ML --- a/src/HOL/Tools/numeral_syntax.ML Tue May 07 14:28:34 2002 +0200 +++ b/src/HOL/Tools/numeral_syntax.ML Tue May 07 14:28:34 2002 +0200 @@ -69,6 +69,9 @@ if not (! show_types) andalso can Term.dest_Type T then t' else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T end + | numeral_tr' _ (*"number_of"*) T (t :: ts) = + if T = dummyT then Syntax.const "_Numeral" $ Syntax.free (dest_bin_str t) + else raise Match | numeral_tr' _ (*"number_of"*) _ _ = raise Match;