diff -r bfcabed9079e -r 949957531f63 ProgTutorial/FirstSteps.thy
--- 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''