# HG changeset patch # User wenzelm # Date 936213986 -7200 # Node ID 8f284fbb8728f559525092e7bd70137657ce0166 # Parent 80838c2af97b577fcdad23496fbef4fc7f78976d observe show_types; diff -r 80838c2af97b -r 8f284fbb8728 src/HOL/Tools/numeral_syntax.ML --- a/src/HOL/Tools/numeral_syntax.ML Wed Sep 01 21:25:55 1999 +0200 +++ b/src/HOL/Tools/numeral_syntax.ML Wed Sep 01 21:26:26 1999 +0200 @@ -91,7 +91,7 @@ fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) = let val t' = Syntax.const "_Numeral" $ (Syntax.const "_xnum" $ Syntax.free (dest_bin_str t)) in - if can Term.dest_Type T then t' + 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"*) _ _ = raise Match;