diff -r fdead18501ca -r 4281ccea43f0 doc-src/TutorialI/Recdef/termination.thy
--- a/doc-src/TutorialI/Recdef/termination.thy	Fri Sep 15 19:34:28 2000 +0200
+++ b/doc-src/TutorialI/Recdef/termination.thy	Fri Sep 15 19:59:05 2000 +0200
@@ -47,7 +47,7 @@
 consts g :: "nat\<times>nat \<Rightarrow> nat";
 recdef g "measure(\<lambda>(x,y). x-y)"
   "g(x,y) = (if x \<le> y then x else g(x,y+1))"
-(hints simp: termi_lem)
+(hints recdef_simp: termi_lem)
 
 text{*\noindent
 This time everything works fine. Now @{thm[source]g.simps} contains precisely