--- a/ProgTutorial/FirstSteps.thy	Mon Mar 23 12:47:05 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Mon Mar 23 13:27:12 2009 +0100
@@ -650,8 +650,8 @@
                 (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}
 
   There are a number of handy functions that are frequently used for 
-  constructing terms. One is the function @{ML list_comb} which a term
-  and a list of terms as argument, and produces as output the term
+  constructing terms. One is the function @{ML list_comb} which takes a term
+  and a list of terms as arguments, and produces as output the term
   list applied to the term. For example
 
 @{ML_response_fake [display,gray]
@@ -688,7 +688,7 @@
 
   \begin{exercise}\label{fun:makesum}
   Write a function which takes two terms representing natural numbers
-  in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produce the
+  in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produces the
   number representing their sum.
   \end{exercise}