diff -r 3489daf839d5 -r 26bdfb7b680b src/HOL/Library/ContNotDenum.thy
--- a/src/HOL/Library/ContNotDenum.thy	Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/Library/ContNotDenum.thy	Mon Jul 12 08:58:13 2010 +0200
@@ -402,7 +402,6 @@
        (f (Suc n)) \<notin> e)
       )"
 
-declare newInt.simps [code del]
 
 subsubsection {* Properties *}