1.1 --- a/src/HOL/Hilbert_Choice.thy	Sun Dec 22 10:43:43 2002 +0100
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Sun Dec 22 15:02:40 2002 +0100
     1.3 @@ -22,7 +22,7 @@
     1.4  syntax
     1.5    "_Eps"        :: "[pttrn, bool] => 'a"    ("(3SOME _./ _)" [0, 10] 10)
     1.6  translations
     1.7 -  "SOME x. P" => "Eps (%x. P)"
     1.8 +  "SOME x. P" == "Eps (%x. P)"
     1.9  
    1.10  print_translation {*
    1.11  (* to avoid eta-contraction of body *)