src/HOL/HOL.thy
changeset 13763 f94b569cd610
parent 13723 c7d104550205
child 13764 3e180bf68496
--- 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)