--- a/CookBook/FirstSteps.thy	Tue Feb 24 01:30:15 2009 +0000
+++ b/CookBook/FirstSteps.thy	Tue Feb 24 11:15:41 2009 +0000
@@ -141,6 +141,7 @@
    Syntax.string_of_term ctxt (term_of t)*}
 
 text {*
+  The function @{ML term_of} extracts the @{ML_type term} from a @{ML_type cterm}.
   If there are more than one @{ML_type cterm}s to be printed, you can use the 
   function @{ML commas} to separate them.
 *} 
@@ -388,7 +389,7 @@
 (?P \<and> ?Q \<and> ?R) = (?Q \<and> ?P \<and> ?R)
 ((?P \<and> ?Q) \<and> ?R) = (?P \<and> ?Q \<and> ?R)"}  
 
-  You can also refer to the current simpsets. To illustrate this we use the
+  You can also refer to the current simpset. To illustrate this we use the
   function that extracts the theorem names stored in a simpset.
 *}
 
@@ -404,8 +405,9 @@
   information about the simpset. The rules of a simpset are stored in a
   \emph{discrimination net} (a data structure for fast indexing). From this
   net you can extract the entries using the function @{ML Net.entries}.
-  You can now use @{ML get_thm_names} to obtain all names of theorems of
-  the current simpset using the antiquotation @{text "@{simpset}"}.\footnote
+  You can now use @{ML get_thm_names} to obtain all names of theorems stored
+  in the current simpset---this simpset can be referred to using the antiquotation
+  @{text "@{simpset}"}.\footnote
   {FIXME: you cannot cleanly match against lists with ommited parts}
 
   @{ML_response_fake [display,gray] 
@@ -571,6 +573,25 @@
 ML{*fun make_fun_type tau1 tau2 = tau1 --> tau2 *}
 
 text {*
+  A handy function for manipulating terms is @{ML map_types}: it takes a 
+  function and applies it to every type in the term. You can, for example,
+  change every @{typ nat} in a term into an @{typ int} using the function:
+*}
+
+ML{*fun nat_to_int t =
+  (case t of
+     @{typ nat} => @{typ int}
+   | Type (s, ts) => Type (s, map nat_to_int ts)
+   | _ => t)*}
+
+text {*
+  An example as follows:
+
+@{ML_response_fake [display,gray] 
+"map_types nat_to_int @{term \"a = (1::nat)\"}" 
+"Const (\"op =\", \"int \<Rightarrow> int \<Rightarrow> bool\")
+           $ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"}
+
   \begin{readmore}
   There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and
   @{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms 
@@ -595,26 +616,6 @@
   number representing their sum.
   \end{exercise}
 
-  A handy function for manipulating terms is @{ML map_types}: it takes a 
-  function and applies it to every type in the term. You can, for example,
-  change every @{typ nat} in a term into an @{typ int} using the function:
-*}
-
-ML{*fun nat_to_int t =
-  (case t of
-     @{typ nat} => @{typ int}
-   | Type (s, ts) => Type (s, map nat_to_int ts)
-   | _ => t)*}
-
-text {*
-  An example as follows:
-
-@{ML_response_fake [display,gray] 
-"map_types nat_to_int @{term \"a = (1::nat)\"}" 
-"Const (\"op =\", \"int \<Rightarrow> int \<Rightarrow> bool\")
-           $ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"}
-
-
   There are a few subtle issues with constants. They usually crop up when
   pattern matching terms or types, or constructing them. While it is perfectly ok
   to write the function @{text is_true} as follows