--- a/src/HOL/Real/ContNotDenum.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Real/ContNotDenum.thy Fri Oct 10 06:45:53 2008 +0200
@@ -403,7 +403,7 @@
(f (Suc n)) \<notin> e)
)"
-declare newInt.simps [code func del]
+declare newInt.simps [code del]
subsubsection {* Properties *}