--- a/ProgTutorial/Solutions.thy	Tue Jul 21 12:05:15 2009 +0200
+++ b/ProgTutorial/Solutions.thy	Tue Jul 21 12:11:24 2009 +0200
@@ -14,6 +14,11 @@
    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} *}
 
 ML{*fun make_sum t1 t2 =
@@ -212,4 +217,4 @@
   rewriting, or when rewriting rules are lead to non-termination.
 *}
 
-end
\ No newline at end of file
+end