diff -r a6fb4ddc05c7 -r 0a4cc9b113c7 doc-src/TutorialI/Overview/LNCS/RECDEF.thy
--- a/doc-src/TutorialI/Overview/LNCS/RECDEF.thy	Mon May 02 10:56:13 2005 +0200
+++ b/doc-src/TutorialI/Overview/LNCS/RECDEF.thy	Mon May 02 11:03:27 2005 +0200
@@ -29,7 +29,7 @@
   "sep1(a, xs)     = xs";
 
 text{*
-This is what the rules for @{term sep1} are turned into:
+This is what the rules for @{const sep1} are turned into:
 @{thm[display,indent=5] sep1.simps[no_vars]}
 *}
 (*<*)