added print translations tha avoid eta contraction for important binders.

--- 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)

--- 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)"

--- a/src/HOL/Set.thy	Sun Dec 22 10:42:09 2002 +0100
+++ b/src/HOL/Set.thy	Sun Dec 22 10:43:43 2002 +0100
@@ -74,15 +74,15 @@
   "x ~: y"      == "~ (x : y)"
   "{x, xs}"     == "insert x {xs}"
   "{x}"         == "insert x {}"
-  "{x. P}"      == "Collect (%x. P)"
+  "{x. P}"      => "Collect (%x. P)"
   "UN x y. B"   == "UN x. UN y. B"
   "UN x. B"     == "UNION UNIV (%x. B)"
   "INT x y. B"  == "INT x. INT y. B"
   "INT x. B"    == "INTER UNIV (%x. B)"
-  "UN x:A. B"   == "UNION A (%x. B)"
-  "INT x:A. B"  == "INTER A (%x. B)"
-  "ALL x:A. P"  == "Ball A (%x. P)"
-  "EX x:A. P"   == "Bex A (%x. P)"
+  "UN x:A. B"   => "UNION A (%x. B)"
+  "INT x:A. B"  => "INTER A (%x. B)"
+  "ALL x:A. P"  => "Ball A (%x. P)"
+  "EX x:A. P"   => "Bex A (%x. P)"
 
 syntax (output)
   "_setle"      :: "'a set => 'a set => bool"             ("op <=")
@@ -150,22 +150,36 @@
   in [("@SetCompr", setcompr_tr)] end;
 *}
 
+(* To avoid eta-contraction of body: *)
 print_translation {*
-  let
-    val ex_tr' = snd (mk_binder_tr' ("Ex", "DUMMY"));
-
-    fun setcompr_tr' [Abs (_, _, P)] =
-      let
-        fun check (Const ("Ex", _) $ Abs (_, _, P), n) = check (P, n + 1)
-          | check (Const ("op &", _) $ (Const ("op =", _) $ Bound m $ e) $ P, n) =
-              if n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso
-                ((0 upto (n - 1)) subset add_loose_bnos (e, 0, [])) then ()
-              else raise Match;
+let
+  fun btr' syn [A,Abs abs] =
+    let val (x,t) = atomic_abs_tr' abs
+    in Syntax.const syn $ x $ A $ t end
+in
+[("Ball", btr' "_Ball"),("Bex", btr' "_Bex"),
+ ("UNION", btr' "@UNION"),("INTER", btr' "@INTER")]
+end
+*}
+
+print_translation {*
+let
+  val ex_tr' = snd (mk_binder_tr' ("Ex", "DUMMY"));
+
+  fun setcompr_tr' [Abs (abs as (_, _, P))] =
+    let
+      fun check (Const ("Ex", _) $ Abs (_, _, P), n) = check (P, n + 1)
+        | check (Const ("op &", _) $ (Const ("op =", _) $ Bound m $ e) $ P, n) =
+            n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso
+            ((0 upto (n - 1)) subset add_loose_bnos (e, 0, []))
 
         fun tr' (_ $ abs) =
           let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr' [abs]
           in Syntax.const "@SetCompr" $ e $ idts $ Q end;
-      in check (P, 0); tr' P end;
+    in if check (P, 0) then tr' P
+       else let val (x,t) = atomic_abs_tr' abs
+            in Syntax.const "@Coll" $ x $ t end
+    end;
   in [("Collect", setcompr_tr')] end;
 *}