# HG changeset patch
# User haftmann
# Date 1442915302 -7200
# Node ID af7bed1360f30bf027054db921ee7f7d150dc5a1
# Parent  1a690dce8cfce5dfdc538ab9bfdec2187cded560
effective revert of e6b1236f9b3d: spontaneous eta-contraction happens on the print translation level and can only be suppressed on the print translation level

diff -r 1a690dce8cfc -r af7bed1360f3 NEWS
--- a/NEWS	Tue Sep 22 14:31:22 2015 +0200
+++ b/NEWS	Tue Sep 22 11:48:22 2015 +0200
@@ -202,16 +202,10 @@
 
 * Combinator to represent case distinction on products is named "uncurry",
 with "split" and "prod_case" retained as input abbreviations.
-Partially applied occurences of "uncurry" with eta-contracted body
-terms are not printed with special syntax, to provide a compact
-notation and getting rid of a special-case print translation.
 Hence, the "uncurry"-expressions are printed the following way:
 a) fully applied "uncurry f p": explicit case-expression;
-b) partially applied with explicit double lambda abstraction in
-the body term "uncurry (%a b. t [a, b])": explicit paired abstraction;
-c) partially applied with eta-contracted body term "uncurry f":
-no special syntax, plain "uncurry" combinator.
-This aims for maximum readability in a given subterm.
+b) partially applied "uncurry f": explicit paired abstraction;
+c) unapplied "uncurry": as it is.
 INCOMPATIBILITY.
 
 * Some old and rarely used ASCII replacement syntax has been removed.
diff -r 1a690dce8cfc -r af7bed1360f3 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Tue Sep 22 14:31:22 2015 +0200
+++ b/src/HOL/Product_Type.thy	Tue Sep 22 11:48:22 2015 +0200
@@ -311,6 +311,41 @@
      The @{text "(x, y)"} is parsed as @{text "Pair x y"} because it is @{text logic},
      not @{text pttrn}.\<close>
 
+text \<open>print @{term "uncurry f"} as @{term "\<lambda>(x, y). f x y"} and
+  @{term "uncurry (\<lambda>x. f x)"} as @{term "\<lambda>(x, y). f x y"}\<close>
+
+typed_print_translation \<open>
+  let
+    fun uncurry_guess_names_tr' T [Abs (x, _, Abs _)] = raise Match
+      | uncurry_guess_names_tr' T [Abs (x, xT, t)] =
+          (case (head_of t) of
+            Const (@{const_syntax uncurry}, _) => raise Match
+          | _ =>
+            let 
+              val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
+              val (y, t') = Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 1 t $ Bound 0);
+              val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, xT, t');
+            in
+              Syntax.const @{syntax_const "_abs"} $
+                (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
+            end)
+      | uncurry_guess_names_tr' T [t] =
+          (case head_of t of
+            Const (@{const_syntax uncurry}, _) => raise Match
+          | _ =>
+            let
+              val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
+              val (y, t') =
+                Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 2 t $ Bound 1 $ Bound 0);
+              val (x', t'') = Syntax_Trans.atomic_abs_tr' ("x", xT, t');
+            in
+              Syntax.const @{syntax_const "_abs"} $
+                (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
+            end)
+      | uncurry_guess_names_tr' _ _ = raise Match;
+  in [(@{const_syntax uncurry}, K uncurry_guess_names_tr')] end
+\<close>
+
 
 subsubsection \<open>Code generator setup\<close>