# HG changeset patch
# User nipkow
# Date 1518076768 -3600
# Node ID b01b22f9e42e7f9874bcbccb9b94324724cf8f49
# Parent  4a3d657adc622b3cbcffdd49f3038e4564513ace# Parent  8563eb539e7fb01a8d076030af3036a082e620c1
merged

diff -r 4a3d657adc62 -r b01b22f9e42e src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Feb 07 18:08:12 2018 +0100
+++ b/src/HOL/Product_Type.thy	Thu Feb 08 08:59:28 2018 +0100
@@ -446,6 +446,11 @@
   \<comment> \<open>Subsumes the old \<open>split_Pair\<close> when @{term f} is the identity function.\<close>
   by (simp add: fun_eq_iff split: prod.split)
 
+(* This looks like a sensible simp-rule but appears to do more harm than good:
+lemma case_prod_const [simp]: "(\<lambda>(_,_). c) = (\<lambda>_. c)"
+by(rule case_prod_eta)
+*)
+
 lemma case_prod_comp: "(case x of (a, b) \<Rightarrow> (f \<circ> g) a b) = f (g (fst x)) (snd x)"
   by (cases x) simp