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)