observe show_types;
authorwenzelm
Wed Sep 01 21:26:26 1999 +0200 (1999-09-01)
changeset 74298f284fbb8728
parent 7428 80838c2af97b
child 7430 6ea8cbf94118
observe show_types;
src/HOL/Tools/numeral_syntax.ML
     1.1 --- a/src/HOL/Tools/numeral_syntax.ML	Wed Sep 01 21:25:55 1999 +0200
     1.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Wed Sep 01 21:26:26 1999 +0200
     1.3 @@ -91,7 +91,7 @@
     1.4  
     1.5  fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =
     1.6        let val t' = Syntax.const "_Numeral" $ (Syntax.const "_xnum" $ Syntax.free (dest_bin_str t)) in
     1.7 -        if can Term.dest_Type T then t'
     1.8 +        if not (! show_types) andalso can Term.dest_Type T then t'
     1.9          else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T
    1.10        end
    1.11    | numeral_tr' _ (*"number_of"*) _ _ = raise Match;