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