--- a/thys/Hoare_tm.thy	Tue Mar 25 11:20:36 2014 +0000
+++ b/thys/Hoare_tm.thy	Thu Mar 27 11:50:37 2014 +0000
@@ -933,11 +933,6 @@
 lemma nth_app: "length xs \<le> a \<Longrightarrow> (xs @ ys)!a = ys!(a - length xs)"
   by (metis not_less nth_append)
 
-(* FIXME in Hoare_gen? *)
-lemma pred_exI: 
-  assumes "(P(x) \<and>* r) s"
-  shows "((EXS x. P(x)) \<and>* r) s"
-  by (metis assms pred_ex_def sep_globalise)
 
 lemma list_ext_tail:
   assumes h1: "length xs \<le> a"