diff -r 8f7d6f01a775 -r 88263522c31e src/HOL/BNF_FP_Base.thy
--- a/src/HOL/BNF_FP_Base.thy	Wed Jun 18 17:42:24 2014 +0200
+++ b/src/HOL/BNF_FP_Base.thy	Wed Jun 18 17:42:24 2014 +0200
@@ -71,9 +71,6 @@
 "case_sum f g (if p then Inl x else Inr y) = (if p then f x else g y)"
 by simp
 
-lemma Inl_Inr_False: "(Inl x = Inr y) = False"
-by simp
-
 lemma prod_set_simps:
 "fsts (x, y) = {x}"
 "snds (x, y) = {y}"