--- a/ProgTutorial/FirstSteps.thy	Tue Jul 21 12:45:17 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Tue Jul 21 12:51:14 2009 +0200
@@ -925,27 +925,6 @@
   "writeln (Syntax.string_of_term @{context}
    (HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"})))"
   "True = False"}
-
-  \begin{readmore}
-  There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and
-  @{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms 
-  and types easier.\end{readmore}
-
-  Have a look at these files and try to solve the following two exercises:
-
-  \begin{exercise}\label{fun:revsum}
-  Write a function @{text "rev_sum : term -> term"} that takes a
-  term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "n"} might be zero)
-  and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume
-  the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"} 
-  associates to the left. Try your function on some examples. 
-  \end{exercise}
-
-  \begin{exercise}\label{fun:makesum}
-  Write a function which takes two terms representing natural numbers
-  in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produces the
-  number representing their sum.
-  \end{exercise}
 *}
 
 section {* Constants *}
@@ -968,7 +947,7 @@
   | is_all _ = false*}
 
 text {* 
-  will not correctly match the formula @{prop "\<forall>x::nat. P x"}: 
+  will not correctly match the formula @{prop[source] "\<forall>x::nat. P x"}: 
 
   @{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "false"}
 
@@ -1034,7 +1013,28 @@
   | is_nil_or_all _ = false *}
 
 text {*
-  The antiquotation for properly referencing type constants is  is @{text "@{type_name \<dots>}"}.
+  \begin{readmore}
+  There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and
+  @{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms 
+  and types easier.\end{readmore}
+
+  Have a look at these files and try to solve the following two exercises:
+
+  \begin{exercise}\label{fun:revsum}
+  Write a function @{text "rev_sum : term -> term"} that takes a
+  term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "n"} might be one)
+  and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume
+  the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"} 
+  associates to the left. Try your function on some examples. 
+  \end{exercise}
+
+  \begin{exercise}\label{fun:makesum}
+  Write a function which takes two terms representing natural numbers
+  in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produces the
+  number representing their sum.
+  \end{exercise}
+
+  The antiquotation for properly referencing type constants is @{text "@{type_name \<dots>}"}.
   For example
 
   @{ML_response [display,gray]
@@ -1183,7 +1183,7 @@
   the file @{ML_file "Pure/thm.ML"}.
   \end{readmore}
 
-  \begin{exercise}
+  \begin{exercise}\label{fun:revsum typed}
   Check that the function defined in Exercise~\ref{fun:revsum} returns a
   result that type-checks.
   \end{exercise}

--- a/ProgTutorial/Solutions.thy	Tue Jul 21 12:45:17 2009 +0200
+++ b/ProgTutorial/Solutions.thy	Tue Jul 21 12:51:14 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