# HG changeset patch
# User haftmann
# Date 1410353823 -7200
# Node ID e7320cceda9c19b2f87057e512bd2a545008a032
# Parent  81a5f05130c11510997c4e8a859d2ebe27df2041
dropped ineffective print_translation which has never been adjusted to check/uncheck-style case patterns

diff -r 81a5f05130c1 -r e7320cceda9c src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Tue Sep 09 23:54:47 2014 +0200
+++ b/src/HOL/Product_Type.thy	Wed Sep 10 14:57:03 2014 +0200
@@ -385,28 +385,6 @@
   in [(@{const_syntax case_prod}, K split_guess_names_tr')] end
 *}
 
-(* Force eta-contraction for terms of the form "Q A (%p. case_prod P p)"
-   where Q is some bounded quantifier or set operator.
-   Reason: the above prints as "Q p : A. case p of (x,y) \<Rightarrow> P x y"
-   whereas we want "Q (x,y):A. P x y".
-   Otherwise prevent eta-contraction.
-*)
-print_translation {*
-  let
-    fun contract Q tr ctxt ts =
-      (case ts of
-        [A, Abs (_, _, (s as Const (@{const_syntax case_prod},_) $ t) $ Bound 0)] =>
-          if Term.is_dependent t then tr ctxt ts
-          else Syntax.const Q $ A $ s
-      | _ => tr ctxt ts);
-  in
-    [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"},
-     Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"},
-     Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFIMUM} @{syntax_const "_INF"},
-     Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPREMUM} @{syntax_const "_SUP"}]
-    |> map (fn (Q, tr) => (Q, contract Q tr))
-  end
-*}
 
 subsubsection {* Code generator setup *}