diff -r 691da43fbdd4 -r 9df717fef2bb src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Sun May 04 16:17:53 2014 +0200
+++ b/src/HOL/Predicate.thy	Sun May 04 18:14:58 2014 +0200
@@ -498,7 +498,7 @@
   "size (P :: 'a Predicate.pred) = 0" by (cases P) simp
 
 lemma [code]:
-  "pred_size f P = 0" by (cases P) simp
+  "size_pred f P = 0" by (cases P) simp
 
 primrec contained :: "'a seq \<Rightarrow> 'a pred \<Rightarrow> bool" where
   "contained Empty Q \<longleftrightarrow> True"