--- a/ProgTutorial/FirstSteps.thy	Mon Jul 20 16:52:59 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Tue Jul 21 12:45:17 2009 +0200
@@ -347,14 +347,19 @@
       |> curry list_comb f *}
 
 text {*
-  This code extracts the argument types of a given function @{text "f"} and then generates 
-  for each argument type a distinct variable; finally it applies the generated 
-  variables to the function. For example:
+  This function takes a term and a context as argument. If the term is of function
+  type, then @{ML "apply_fresh_args"} returns the term with distinct variables 
+  applied to it. For example:
 
   @{ML_response_fake [display,gray]
-"apply_fresh_args @{term \"P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool\"} @{context} 
- |> Syntax.string_of_term @{context}
- |> writeln"
+"let
+  val t = @{term \"P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool\"}
+  val ctxt = @{context}
+in 
+  apply_fresh_args t ctxt
+   |> Syntax.string_of_term ctxt
+   |> writeln
+end" 
   "P z za zb"}
 
   You can read off this behaviour from how @{ML apply_fresh_args} is
@@ -372,11 +377,18 @@
   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"
+"let
+  val t = @{term \"za::'a \<Rightarrow> 'b \<Rightarrow> 'c\"}
+  val ctxt = @{context}
+in
+  apply_fresh_args t ctxt 
+   |> Syntax.string_of_term ctxt
+   |> writeln
+end"
   "za z zb"}
   
+  where the @{text "za"} is correctly avoided.
+
   The combinator @{ML [index] "#>"} is the reverse function composition. It can be
   used to define the following function
 *}