src/HOL/Datatype.thy
changeset 18757 f0d901bc0686
parent 18702 7dc7dcd63224
child 19111 1f6112de1d0f
     1.1 --- a/src/HOL/Datatype.thy	Mon Jan 23 14:06:40 2006 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Mon Jan 23 14:07:52 2006 +0100
     1.3 @@ -224,16 +224,16 @@
     1.4  
     1.5  code_syntax_const
     1.6    True
     1.7 -    ml (atom "true")
     1.8 -    haskell (atom "True")
     1.9 +    ml (target_atom "true")
    1.10 +    haskell (target_atom "True")
    1.11    False
    1.12 -    ml (atom "false")
    1.13 -    haskell (atom "False")
    1.14 +    ml (target_atom "false")
    1.15 +    haskell (target_atom "False")
    1.16  
    1.17  code_syntax_const
    1.18    Pair
    1.19 -    ml (atom "(__,/ __)")
    1.20 -    haskell (atom "(__,/ __)")
    1.21 +    ml (target_atom "(__,/ __)")
    1.22 +    haskell (target_atom "(__,/ __)")
    1.23  
    1.24  code_syntax_const
    1.25    1 :: "nat"