diff -r dfc7a46c2900 -r 32e0da92c786 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Thu Apr 03 10:51:20 2014 +0200
+++ b/src/HOL/Wellfounded.thy	Thu Apr 03 10:51:22 2014 +0200
@@ -859,7 +859,7 @@
 lemma nat_size [simp, code]: "size (n\<Colon>nat) = n"
   by (induct n) simp_all
 
-declare "prod.size" [no_atp]
+declare prod.size [no_atp]
 
 
 hide_const (open) acc accp