--- a/src/HOL/Hilbert_Choice.thy Sun Dec 22 10:42:09 2002 +0100
+++ b/src/HOL/Hilbert_Choice.thy Sun Dec 22 10:43:43 2002 +0100
@@ -22,7 +22,14 @@
syntax
"_Eps" :: "[pttrn, bool] => 'a" ("(3SOME _./ _)" [0, 10] 10)
translations
- "SOME x. P" == "Eps (%x. P)"
+ "SOME x. P" => "Eps (%x. P)"
+
+print_translation {*
+(* to avoid eta-contraction of body *)
+[("Eps", fn [Abs abs] =>
+ let val (x,t) = atomic_abs_tr' abs
+ in Syntax.const "_Eps" $ x $ t end)]
+*}
axioms
someI: "P (x::'a) ==> P (SOME x. P x)"