--- a/src/HOL/HOL.thy Sun Dec 22 10:42:09 2002 +0100
+++ b/src/HOL/HOL.thy Sun Dec 22 10:43:43 2002 +0100
@@ -71,10 +71,17 @@
translations
"x ~= y" == "~ (x = y)"
- "THE x. P" == "The (%x. P)"
+ "THE x. P" => "The (%x. P)"
"_Let (_binds b bs) e" == "_Let b (_Let bs e)"
"let x = a in e" == "Let a (%x. e)"
+print_translation {*
+(* To avoid eta-contraction of body: *)
+[("The", fn [Abs abs] =>
+ let val (x,t) = atomic_abs_tr' abs
+ in Syntax.const "_The" $ x $ t end)]
+*}
+
syntax (output)
"=" :: "['a, 'a] => bool" (infix 50)
"_not_equal" :: "['a, 'a] => bool" (infix "~=" 50)