--- a/CookBook/FirstSteps.thy	Tue Mar 17 17:32:12 2009 +0100
+++ b/CookBook/FirstSteps.thy	Wed Mar 18 03:03:51 2009 +0100
@@ -261,8 +261,8 @@
        |> (curry list_comb) pred *}
 
 text {*
-  This code extracts the argument types of the given
-  predicate and then generate for each type a distinct variable; finally it
+  This code extracts the argument types of a given
+  predicate and then generates for each argument type a distinct variable; finally it
   applies the generated variables to the predicate. For example
 
   @{ML_response_fake [display,gray]
@@ -271,17 +271,17 @@
  |> warning"
   "P z za zb"}
 
-  You can read this off this behaviour from how @{ML apply_fresh_args} is
+  You can read 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
+  predicate; @{ML binder_types} in the next line 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
+  unique name avoiding the given @{text pred}; the list of name-type pairs is turned
+  into a list of variable terms in Line 6, which in the last line is 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.
+  variables list as a pair.
   
   The combinator @{ML "#>"} is the reverse function composition. It can be
   used to define the following function
@@ -443,9 +443,9 @@
 
 text {*
   The function @{ML dest_ss in MetaSimplifier} returns a record containing all
-  information stored in the simpset. We are only interested in the You can now use @{ML get_thm_names_from_ss} to obtain all names of theorems stored
-  in the current simpset. This simpset can be referred to using the antiquotation
-  @{text "@{simpset}"}.
+  information stored in the simpset. We are only interested in the names of the
+  simp-rules. So now you can feed in the current simpset into this function. 
+  The simpset can be referred to using the antiquotation @{text "@{simpset}"}.
 
   @{ML_response_fake [display,gray] 
   "get_thm_names_from_ss @{simpset}" 
@@ -596,7 +596,7 @@
     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})
+  (FIXME: handy functions for constructing terms: @{ML list_comb}, @{ML lambda})
 
 
   Although types of terms can often be inferred, there are many