1.1 --- a/src/HOL/Library/ContNotDenum.thy	Mon Jul 12 08:58:12 2010 +0200
     1.2 +++ b/src/HOL/Library/ContNotDenum.thy	Mon Jul 12 08:58:13 2010 +0200
     1.3 @@ -402,7 +402,6 @@
     1.4         (f (Suc n)) \<notin> e)
     1.5        )"
     1.6  
     1.7 -declare newInt.simps [code del]
     1.8  
     1.9  subsubsection {* Properties *}
    1.10