# HG changeset patch
# User nipkow
# Date 1518076756 -3600
# Node ID 8563eb539e7fb01a8d076030af3036a082e620c1
# Parent  ed0a7090167d21d0af2f5a735b9389920e3d6349
tuned

diff -r ed0a7090167d -r 8563eb539e7f src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Mon Feb 05 08:30:19 2018 +0100
+++ b/src/HOL/Product_Type.thy	Thu Feb 08 08:59:16 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