diff -r 480b2de9927c -r 254a021ed66e doc-src/TutorialI/ToyList/ToyList.thy
--- a/doc-src/TutorialI/ToyList/ToyList.thy	Wed Aug 11 14:45:38 2010 +0200
+++ b/doc-src/TutorialI/ToyList/ToyList.thy	Sun Aug 15 16:48:42 2010 +0200
@@ -105,6 +105,8 @@
 When Isabelle prints a syntax error message, it refers to the HOL syntax as
 the \textbf{inner syntax} and the enclosing theory language as the \textbf{outer syntax}.
 
+Comments\index{comment} must be in enclosed in \texttt{(* }and\texttt{ *)}.
+
 \section{Evaluation}
 \index{evaluation}
 
@@ -120,17 +122,7 @@
 But we can go beyond mere functional programming and evaluate terms with
 variables in them, executing functions symbolically: *}
 
-normal_form "rev (a # b # c # [])"
-
-text{*\noindent yields @{term"c # b # a # []"}.
-Command \commdx{normal\protect\_form} works for arbitrary terms
-but can be slower than command \commdx{value},
-which is restricted to variable-free terms and executable functions.
-To appreciate the subtleties of evaluating terms with variables,
-try this one:
-*}
-
-normal_form "rev (a # b # c # xs)"
+value "rev (a # b # c # [])"
 
 text{*
 \section{An Introductory Proof}