diff -r 41a802bbb7df -r 0a567f923b42 ProgTutorial/Intro.thy
--- a/ProgTutorial/Intro.thy	Tue Jul 28 08:53:05 2009 +0200
+++ b/ProgTutorial/Intro.thy	Tue Jul 28 12:11:33 2009 +0200
@@ -211,10 +211,10 @@
   \item {\bf Armin Heller} helped with recipe \ref{rec:sat}.
 
   \item {\bf Alexander Krauss} wrote the first version of the ``first-steps'' 
-  chapter and also contributed the material on @{text NamedThmsFun}.
+  chapter and also contributed the material on @{ML_functor Named_Thms}.
 
   \item {\bf Christian Sternagel} proofread the tutorial and made 
-  many comments on the text. 
+  many improvemets to the text. 
   \end{itemize}
 
   Please let me know of any omissions. Responsibility for any remaining