diff -r 831d4c259f5f -r 669a820ef213 src/HOL/Codatatype/BNF_Library.thy
--- a/src/HOL/Codatatype/BNF_Library.thy	Mon Sep 10 17:36:02 2012 +0200
+++ b/src/HOL/Codatatype/BNF_Library.thy	Mon Sep 10 17:52:01 2012 +0200
@@ -829,6 +829,9 @@
 lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
 by simp
 
+lemma obj_one_pointE: "\<forall>x. s = x \<longrightarrow> P \<Longrightarrow> P"
+by blast
+
 lemma obj_sumE_f:
 "\<lbrakk>\<forall>x. s = f (Inl x) \<longrightarrow> P; \<forall>x. s = f (Inr x) \<longrightarrow> P\<rbrakk> \<Longrightarrow> \<forall>x. s = f x \<longrightarrow> P"
 by (metis sum.exhaust)