--- a/ProgTutorial/FirstSteps.thy	Tue Jul 21 12:11:24 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Tue Jul 21 12:27:12 2009 +0200
@@ -1001,11 +1001,6 @@
   the file @{ML_file "Pure/thm.ML"}.
   \end{readmore}
 
-  \begin{exercise}
-  Check that the function defined in Exercise~\ref{fun:revsum} returns a
-  result that type-checks.
-  \end{exercise}
-
   Remember Isabelle follows the Church-style typing for terms, i.e., a term contains 
   enough typing information (constants, free variables and abstractions all have typing 
   information) so that it is always clear what the type of a term is. 
@@ -1038,6 +1033,11 @@
 
   where no error is detected.
 
+  \begin{exercise}\label{fun:revsum typed}
+  Check that the function defined in Exercise~\ref{fun:revsum} returns a
+  result that type-checks.
+  \end{exercise}
+
   Sometimes it is a bit inconvenient to construct a term with 
   complete typing annotations, especially in cases where the typing 
   information is redundant. A short-cut is to use the ``place-holder'' 

--- 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} *}
 

Binary file progtutorial.pdf has changed