src/HOL/Real/ContNotDenum.thy

        e = closed_int e1 e2 \<and>
        e \<subseteq> (newInt n f) \<and>
        (f (Suc n)) \<notin> e)
       )"
 
-declare newInt.simps [code func del]
+declare newInt.simps [code del]
 
 subsubsection {* Properties *}
 
 text {* We now show that every application of newInt returns an
 appropriate interval. *}