# 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;