
diff -r f552152d7747 -r 46cfc4b8112e src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Wellfounded.thy	Thu Mar 18 12:58:52 2010 +0100
@@ -908,7 +908,7 @@
 lemma nat_size [simp, code]: "size (n\<Colon>nat) = n"
   by (induct n) simp_all
 
-declare "prod.size" [noatp]
+declare "prod.size" [no_atp]
 
 lemma [code]:
   "size (P :: 'a Predicate.pred) = 0" by (cases P) simp




