diff -r 218e3943d504 -r 0f9534b7ea75 doc-src/Functions/Thy/Functions.thy
--- a/doc-src/Functions/Thy/Functions.thy	Fri May 27 16:45:24 2011 +0200
+++ b/doc-src/Functions/Thy/Functions.thy	Fri May 27 21:11:44 2011 +0200
@@ -558,6 +558,7 @@
 *}
 
 by auto
+termination by (relation "{}") simp
 
 
 subsection {* Non-constructor patterns *}
@@ -685,6 +686,7 @@
   "check (''good'') = True"
 | "s \<noteq> ''good'' \<Longrightarrow> check s = False"
 by auto
+termination by (relation "{}") simp
 
 
 section {* Partiality *}