diff -r c354e45d80d2 -r 2ff4867c00cf ProgTutorial/Solutions.thy
--- a/ProgTutorial/Solutions.thy	Mon Jul 20 16:52:59 2009 +0200
+++ b/ProgTutorial/Solutions.thy	Tue Jul 21 12:49:26 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,6 +19,8 @@
    foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t)
 end *}
 
+
+
 text {* \solution{fun:makesum} *}
 
 ML{*fun make_sum t1 t2 =
@@ -212,4 +219,4 @@
   rewriting, or when rewriting rules are lead to non-termination.
 *}
 
-end
\ No newline at end of file
+end