src/HOL/Datatype.thy
changeset 21126 4dbc3ccbaab0
parent 21111 624ed9c7c4fe
child 21243 afffe1f72143
     1.1 --- a/src/HOL/Datatype.thy	Tue Oct 31 14:58:12 2006 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Tue Oct 31 14:58:14 2006 +0100
     1.3 @@ -773,18 +773,18 @@
     1.4  code_const True and False and Not and "op &" and "op |" and If
     1.5    (SML "true" and "false" and "not"
     1.6      and infixl 1 "andalso" and infixl 0 "orelse"
     1.7 -    and "!(if __/ then __/ else __)")
     1.8 +    and "!(if (_)/ then (_)/ else (_))")
     1.9    (Haskell "True" and "False" and "not"
    1.10      and infixl 3 "&&" and infixl 2 "||"
    1.11 -    and "!(if __/ then __/ else __)")
    1.12 +    and "!(if (_)/ then (_)/ else (_))")
    1.13  
    1.14  code_type *
    1.15    (SML infix 2 "*")
    1.16 -  (Haskell "!(__,/ __)")
    1.17 +  (Haskell "!((_),/ (_))")
    1.18  
    1.19  code_const Pair
    1.20 -  (SML "!(__,/ __)")
    1.21 -  (Haskell "!(__,/ __)")
    1.22 +  (SML "!((_),/ (_))")
    1.23 +  (Haskell "!((_),/ (_))")
    1.24  
    1.25  code_type unit
    1.26    (SML "unit")