diff -r b368a7aee46a -r b0d6acf73588 doc-src/Functions/Thy/Functions.thy
--- a/doc-src/Functions/Thy/Functions.thy	Fri Feb 25 16:59:48 2011 +0100
+++ b/doc-src/Functions/Thy/Functions.thy	Fri Feb 25 17:11:05 2011 +0100
@@ -706,7 +706,6 @@
 where
   "findzero f n = (if f n = 0 then n else findzero f (Suc n))"
 by pat_completeness auto
-(*<*)declare findzero.simps[simp del](*>*)
 
 text {*
   \noindent Clearly, any attempt of a termination proof must fail. And without