# HG changeset patch
# User berghofe
# Date 1223913119 -7200
# Node ID d5c090b9a2b1298da97e3e21df02a231ae59203f
# Parent  527fc0af45e3e6ea6b2994615fb9d61bcb5b4bcc
Tuned.

diff -r 527fc0af45e3 -r d5c090b9a2b1 CookBook/Package/Ind_Interface.thy
--- 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:
diff -r 527fc0af45e3 -r d5c090b9a2b1 CookBook/Solutions.thy
--- 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)