--- a/CookBook/Package/Ind_Interface.thy	Mon Oct 13 17:51:09 2008 +0200
+++ b/CookBook/Package/Ind_Interface.thy	Mon Oct 13 17:51:59 2008 +0200
@@ -355,7 +355,7 @@
 Most of the time, however, we will have to deal with tokens that are not just strings.
 The parsers for the theory syntax, as well as the parsers for the argument syntax
 of proof methods and attributes use the token type @{ML_type OuterParse.token},
-which is identical to the type @{ML_type OuterLex.token}.
+which is identical to @{ML_type OuterLex.token}.
 The parser functions for the theory syntax are contained in the structure
 @{ML_struct OuterParse} defined in the file @{ML_file "Pure/Isar/outer_parse.ML"}.
 In our parser, we will use the following functions:

--- a/CookBook/Solutions.thy	Mon Oct 13 17:51:09 2008 +0200
+++ b/CookBook/Solutions.thy	Mon Oct 13 17:51:59 2008 +0200
@@ -9,8 +9,7 @@
 ML {* 
   fun rev_sum t =
   let
-   fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = 
-                                                      u' :: dest_sum u
+   fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u
      | dest_sum u = [u]
    in
      foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t)