--- a/ProgTutorial/FirstSteps.thy	Tue Jul 21 11:53:41 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Tue Jul 21 11:59:09 2009 +0200
@@ -786,27 +786,6 @@
   @{term \"(\<lambda>x::nat. x)\"}"
   "Free (\"x\", \"nat\")"}
 
-  \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}
-
   There are a few subtle issues with constants. They usually crop up when
   pattern matching terms or types, or when constructing them. While it is perfectly ok
   to write the function @{text is_true} as follows
@@ -890,6 +869,27 @@
   | is_nil_or_all _ = false *}
 
 text {*
+  \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}
+
   Occasionally you have to calculate what the ``base'' name of a given
   constant is. For this you can use the function @{ML Sign.extern_const} or
   @{ML Long_Name.base_name}. For example: