--- a/CookBook/Solutions.thy	Wed Jan 14 16:46:07 2009 +0000
+++ b/CookBook/Solutions.thy	Wed Jan 14 17:47:49 2009 +0000
@@ -6,27 +6,22 @@
 
 text {* \solution{fun:revsum} *}
 
-ML {* 
-fun rev_sum t =
+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;
-*}
+ end *}
 
 text {* \solution{fun:makesum} *}
 
-ML {*
-fun make_sum t1 t2 =
-    HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2)
-*}
+ML{*fun make_sum t1 t2 =
+    HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *}
 
 text {* \solution{ex:scancmts} *}
 
-ML {*
-val any = Scan.one (Symbol.not_eof);
+ML{*val any = Scan.one (Symbol.not_eof);
 
 val scan_cmt =
   let
@@ -39,8 +34,7 @@
 
 val scan_all =
   Scan.finite Symbol.stopper (Scan.repeat (scan_cmt || any)) 
-    >> implode #> fst 
-*}
+    >> implode #> fst *}
 
 text {*
   By using @{text "#> fst"} in the last line, the function