--- a/CookBook/FirstSteps.thy	Tue Mar 17 12:26:34 2009 +0100
+++ b/CookBook/FirstSteps.thy	Tue Mar 17 17:32:12 2009 +0100
@@ -261,19 +261,27 @@
        |> (curry list_comb) pred *}
 
 text {*
-  The point of this code is to extract the argument types of the given
+  This code extracts the argument types of the given
   predicate and then generate for each type a distinct variable; finally it
-  applies the generated variables to the predicate. You can read this off from
-  how the function is coded: in Line 2, the function @{ML fastype_of}
-  calculates the type of the predicate; in Line 3, @{ML binder_types} produces
-  the list of argument types; Line 4 pairs up each type with the string (or name)
-  @{text "z"}; the function @{ML variant_frees in Variable} generates for each
-  @{text "z"} a unique name avoiding @{text pred}; the list of name-type pairs
-  is turned into a list of variable terms in Line 6, which in the last line
-  are applied by the function @{ML list_comb} to the predicate. We have to use
-  the function @{ML curry}, because @{ML list_comb} expects the predicate and
-  the argument list as a pair.
+  applies the generated variables to the predicate. 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}
+ |> warning"
+  "P z za zb"}
 
+  You can read this off this behaviour from how @{ML apply_fresh_args} is
+  coded: in Line 2, the function @{ML fastype_of} calculates the type of the
+  predicate; in Line 3, @{ML binder_types} produces the list of argument
+  types (in the case above the list @{text "[nat, int, unit]"}); Line 4 pairs up each 
+  type with the string  @{text "z"}; the
+  function @{ML variant_frees in Variable} generates for each @{text "z"} a
+  unique name avoiding @{text pred}; the list of name-type pairs is turned
+  into a list of variable terms in Line 6, which in the last line are applied
+  by the function @{ML list_comb} to the predicate. We have to use the
+  function @{ML curry}, because @{ML list_comb} expects the predicate and the
+  argument list as a pair.
   
   The combinator @{ML "#>"} is the reverse function composition. It can be
   used to define the following function
@@ -463,6 +471,10 @@
   kinds of logical elements from th ML-level.
 *}
 
+text {*
+  (FIXME: say something about @{text "@{binding \<dots>}"}
+*}
+
 section {* Terms and Types *}
 
 text {*
@@ -584,6 +596,9 @@
     Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ 
                (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}
 
+  (FIXME: handy functions for constructing terms @{ML list_comb}, @{ML lambda})
+
+
   Although types of terms can often be inferred, there are many
   situations where you need to construct types manually, especially  
   when defining constants. For example the function returning a function