--- a/ProgTutorial/FirstSteps.thy	Mon Oct 26 00:00:26 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Tue Oct 27 15:43:21 2009 +0100
@@ -674,8 +674,9 @@
 *}
 
 text {*
-  In this example we obtain three terms whose variables @{text m} and @{text
-  n} are of type @{typ "nat"}. If you have only a single term, then @{ML
+  In this example we obtain three terms (using @{ML_ind parse_term in Syntax}) whose 
+  variables @{text m} and @{text n} are of type @{typ "nat"}. If you have only 
+  a single term, then @{ML
   check_terms in Syntax} needs plumbing. This can be done with the function
   @{ML singleton}.\footnote{There is already a function @{ML check_term in
   Syntax} in the Isabelle sources that is defined in terms of @{ML singleton}