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\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