# HG changeset patch
# User nipkow
# Date 1442934793 -7200
# Node ID e367b93f78e5588c86234c80cd05fbc7f8688c93
# Parent  e602ad53915534b1ef19e3992e20da010077ee10# Parent  0b9c45c4af29787d5a5494e7e07e1ba02f3a7b7f
merged

diff -r 0b9c45c4af29 -r e367b93f78e5 NEWS
--- a/NEWS	Tue Sep 22 17:13:01 2015 +0200
+++ b/NEWS	Tue Sep 22 17:13:13 2015 +0200
@@ -185,7 +185,7 @@
 
 * Abbreviations in type classes now carry proper sort constraint.
 Rare INCOMPATIBILITY in situations where the previous misbehaviour
-has been exploited previously.
+has been exploited.
 
 * Refinement of user-space type system in type classes: pseudo-local
 operations behave more similar to abbreviations.  Potential
@@ -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 0b9c45c4af29 -r e367b93f78e5 src/HOL/Codegenerator_Test/Candidates.thy
--- a/src/HOL/Codegenerator_Test/Candidates.thy	Tue Sep 22 17:13:01 2015 +0200
+++ b/src/HOL/Codegenerator_Test/Candidates.thy	Tue Sep 22 17:13:13 2015 +0200
@@ -8,6 +8,8 @@
   Complex_Main
   "~~/src/HOL/Library/Library"
   "~~/src/HOL/Library/Sublist_Order"
+  "~~/src/HOL/Data_Structures/Tree_Map"
+  "~~/src/HOL/Data_Structures/Tree_Set"
   "~~/src/HOL/Number_Theory/Eratosthenes"
   "~~/src/HOL/ex/Records"
 begin
diff -r 0b9c45c4af29 -r e367b93f78e5 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Tue Sep 22 17:13:01 2015 +0200
+++ b/src/HOL/Product_Type.thy	Tue Sep 22 17:13:13 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>