diff -r 81e2d73f7191 -r 4daf913fdbe1 CookBook/Solutions.thy
--- a/CookBook/Solutions.thy	Wed Oct 29 21:51:25 2008 +0100
+++ b/CookBook/Solutions.thy	Thu Oct 30 13:36:51 2008 +0100
@@ -7,20 +7,20 @@
 text {* \solution{fun:revsum} *}
 
 ML {* 
-  fun rev_sum t =
-  let
-   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)
-   end;
+fun rev_sum t =
+let
+ 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)
+ end;
 *}
 
 text {* \solution{fun:makesum} *}
 
 ML {*
-  fun make_sum t1 t2 =
-      HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2)
+fun make_sum t1 t2 =
+    HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2)
 *}
 
 end
\ No newline at end of file