# HG changeset patch
# User haftmann
# Date 1441570491 -7200
# Node ID e6b1236f9b3daae4e770411ee6a22c7888ec46b2
# Parent  4c68426800de5feb2a74ddc344c109262c7ace4f
obsolete: if case_prod is fully applied, it is printed as proper case expression;
eta-contracted variants are read best as "uncurry" combinator

diff -r 4c68426800de -r e6b1236f9b3d NEWS
--- a/NEWS	Sun Sep 06 22:14:51 2015 +0200
+++ b/NEWS	Sun Sep 06 22:14:51 2015 +0200
@@ -189,6 +189,16 @@
 
 * 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.
 INCOMPATIBILITY.
 
 * Some old and rarely used ASCII replacement syntax has been removed.
@@ -199,6 +209,11 @@
   type_notation Map.map  (infixr "~=>" 0)
   notation Map.map_comp  (infixl "o'_m" 55)
 
+* Case combinator "prod_case" with eta-contracted body functions
+has explicit "uncurry" notation, to provide a compact notation while
+getting ride of a special case translation.  Slight syntactic
+INCOMPATIBILITY.
+
 * Theory Map: lemma map_of_is_SomeD was a clone of map_of_SomeD and has
 been removed. INCOMPATIBILITY.
 
diff -r 4c68426800de -r e6b1236f9b3d src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Sun Sep 06 22:14:51 2015 +0200
+++ b/src/HOL/Product_Type.thy	Sun Sep 06 22:14:51 2015 +0200
@@ -311,39 +311,6 @@
      The @{text "(x, y)"} is parsed as @{text "Pair x y"} because it is @{text logic},
      not @{text pttrn}.\<close>
 
-(* print "split f" as "\<lambda>(x,y). f x y" and "split (\<lambda>x. f x)" as "\<lambda>(x,y). f x y" *) 
-typed_print_translation \<open>
-  let
-    fun split_guess_names_tr' T [Abs (x, _, Abs _)] = raise Match
-      | split_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)
-      | split_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)
-      | split_guess_names_tr' _ _ = raise Match;
-  in [(@{const_syntax uncurry}, K split_guess_names_tr')] end
-\<close>
-
 
 subsubsection \<open>Code generator setup\<close>