diff -r 3da5f3f07d8b -r 4e2341f6599d CookBook/FirstSteps.thy
--- a/CookBook/FirstSteps.thy	Fri Mar 13 16:57:16 2009 +0100
+++ b/CookBook/FirstSteps.thy	Sat Mar 14 00:48:22 2009 +0100
@@ -248,11 +248,35 @@
   avoided: it is more than easy to get the intermediate values wrong, not to 
   mention the nightmares the maintenance of this code causes!
 
+  A ``real world'' example for a function written in the waterfall fashion might
+  be the following:
+*}
 
-  (FIXME: give a real world example involving theories)
+ML %linenosgray{*fun apply_fresh_args pred ctxt =
+  pred |> fastype_of
+       |> binder_types 
+       |> map (pair "z")
+       |> Variable.variant_frees ctxt [pred]
+       |> map Free  
+       |> (curry list_comb) pred *}
 
-  Similarly, the combinator @{ML "#>"} is the reverse function 
-  composition. It can be used to define the following function
+text {*
+  The point of this function is to extract 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/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.
+
+  
+  The combinator @{ML "#>"} is the reverse function composition. It can be
+  used to define the following function
 *}
 
 ML{*val inc_by_six = 
@@ -800,7 +824,7 @@
   @{ML_response [display,gray] 
   "fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}
 
-  However, efficiency is gained on the expense of skiping some tests. You 
+  However, efficiency is gained on the expense of skipping some tests. You 
   can see this in the following example
 
    @{ML_response [display,gray] 
@@ -944,8 +968,7 @@
   using the function @{ML Attrib.add_attributes} as follows.
 *}
 
-setup {*
-  Attrib.add_attributes 
+setup %gray {* Attrib.add_attributes 
     [("my_sym", Attrib.no_args my_symmetric, "applying the sym rule")] *}
 
 text {*
@@ -1012,10 +1035,9 @@
   and set up the attributes as follows
 *}
 
-setup {*
-  Attrib.add_attributes 
-    [("my_thms", Attrib.add_del_args my_add my_del, 
-        "maintaining a list of my_thms")] *}
+setup %gray {* Attrib.add_attributes 
+          [("my_thms", Attrib.add_del_args my_add my_del, 
+              "maintaining a list of my_thms")] *}
 
 text {*
   Now if you prove the lemma attaching the attribute @{text "[my_thms]"}
@@ -1094,7 +1116,7 @@
   and set up the @{ML_struct FooRules} with the command
 *}
 
-setup {* FooRules.setup *}
+setup %gray {* FooRules.setup *}
 
 text {*
   This code declares a data slot where the theorems are stored,