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>