src/HOL/Wellfounded.thy

--- a/src/HOL/Wellfounded.thy	Fri Feb 24 22:46:16 2012 +0100
+++ b/src/HOL/Wellfounded.thy	Fri Feb 24 22:46:44 2012 +0100
@@ -858,10 +858,4 @@
 
 declare "prod.size" [no_atp]
 
-lemma [code]:
-  "size (P :: 'a Predicate.pred) = 0" by (cases P) simp
-
-lemma [code]:
-  "pred_size f P = 0" by (cases P) simp
-
 end