--- a/ProgTutorial/Solutions.thy	Tue Jul 28 08:53:05 2009 +0200
+++ b/ProgTutorial/Solutions.thy	Tue Jul 28 12:11:33 2009 +0200
@@ -6,10 +6,13 @@
 
 text {* \solution{fun:revsum} *}
 
-ML{*fun rev_sum((p as Const(@{const_name plus},_)) $ t $ u) = p $ u $ rev_sum t
+ML{*fun rev_sum ((p as Const (@{const_name plus}, _)) $ t $ u) = 
+      p $ u $ rev_sum t
   | rev_sum t = t *}
 
-text {* \solution{fun:revsum typed} *}
+text {* 
+  An alternative solution using the function @{ML [index] mk_binop in HOLogic} is:
+ *}
 
 ML{*fun rev_sum t =
 let
@@ -19,8 +22,6 @@
    foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t)
 end *}
 
-
-
 text {* \solution{fun:makesum} *}
 
 ML{*fun make_sum t1 t2 =