diff -r cccb25ee1309 -r f380b13b25a7 ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Mon May 18 05:21:40 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Sat May 23 02:19:54 2009 +0200
@@ -344,7 +344,15 @@
   into a list of variable terms in Line 6, which in the last line is applied
   by the function @{ML list_comb} to the function. In this last step we have to 
   use the function @{ML curry}, because @{ML list_comb} expects the function and the
-  variables list as a pair.
+  variables list as a pair. This kind of functions is often needed when
+  constructing terms and the infrastructure helps tremendously to avoid
+  any name clashes. Consider for example: 
+
+   @{ML_response_fake [display,gray]
+"apply_fresh_args @{term \"za::'a \<Rightarrow> 'b \<Rightarrow> 'c\"} @{context} 
+ |> Syntax.string_of_term @{context}
+ |> writeln"
+  "za z zb"}
   
   The combinator @{ML "#>"} is the reverse function composition. It can be
   used to define the following function
@@ -997,11 +1005,11 @@
   change every @{typ nat} in a term into an @{typ int} using the function:
 *}
 
-ML{*fun nat_to_int t =
-  (case t of
+ML{*fun nat_to_int ty =
+  (case ty of
      @{typ nat} => @{typ int}
-   | Type (s, ts) => Type (s, map nat_to_int ts)
-   | _ => t)*}
+   | Type (s, tys) => Type (s, map nat_to_int tys)
+   | _ => ty)*}
 
 text {*
   Here is an example:
@@ -1321,7 +1329,7 @@
   context (which we ignore in the code above) and a theorem (@{text thm}), and 
   returns another theorem (namely @{text thm} resolved with the theorem 
   @{thm [source] sym}: @{thm sym[no_vars]}).\footnote{The function @{ML RS} is explained
-  later on in Section~\ref{sec:simpletacs}.} The function 
+  in Section~\ref{sec:simpletacs}.} The function 
   @{ML "Thm.rule_attribute"} then returns 
   an attribute.