--- a/ProgTutorial/Solutions.thy	Tue Jul 21 12:11:24 2009 +0200
+++ b/ProgTutorial/Solutions.thy	Tue Jul 21 12:27:12 2009 +0200
@@ -6,6 +6,11 @@
 
 text {* \solution{fun:revsum} *}
 
+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} *}
+
 ML{*fun rev_sum t =
 let
   fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u
@@ -14,10 +19,7 @@
    foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t)
 end *}
 
-(* Alternative Solution:
-fun rev_sum((plus as Const(@{const_name plus},_)) $ t $ u) = plus $ u $ rev_sum t
-  | rev_sum t = t
-*)
+
 
 text {* \solution{fun:makesum} *}