diff -r f25ac7194f71 -r a123a64cadeb doc-src/TutorialI/Recdef/Nested1.thy
--- a/doc-src/TutorialI/Recdef/Nested1.thy	Wed Aug 30 18:05:20 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Nested1.thy	Wed Aug 30 18:09:20 2000 +0200
@@ -1,12 +1,12 @@
 (*<*)
 theory Nested1 = Nested0:;
 (*>*)
-consts trev  :: "('a,'b)term => ('a,'b)term";
+consts trev  :: "('a,'b)term \<Rightarrow> ('a,'b)term";
 
 text{*\noindent
 Although the definition of @{term"trev"} is quite natural, we will have
 overcome a minor difficulty in convincing Isabelle of is termination.
-It is precisely this difficulty that is the \textit{rasion d'\^etre} of
+It is precisely this difficulty that is the \textit{raison d'\^etre} of
 this subsection.
 
 Defining @{term"trev"} by \isacommand{recdef} rather than \isacommand{primrec}
@@ -15,30 +15,30 @@
 *};
 
 recdef trev "measure size"
- "trev (Var x) = Var x"
+ "trev (Var x)    = Var x"
  "trev (App f ts) = App f (rev(map trev ts))";
 
-text{*
-FIXME: recdef should complain and generate unprovable termination condition!
-moveto todo
-
+text{*\noindent
 Remember that function @{term"size"} is defined for each \isacommand{datatype}.
-However, the definition does not succeed. Isabelle complains about an unproved termination
-condition
+However, the definition does not succeed. Isabelle complains about an
+unproved termination condition
 \begin{quote}
-@{term[display]"t : set ts --> size t < Suc (term_size ts)"}
+@{term[display]"t : set ts --> size t < Suc (term_list_size ts)"}
 \end{quote}
-where @{term"set"} returns the set of elements of a list---no special knowledge of sets is
-required in the following.
-First we have to understand why the recursive call of @{term"trev"} underneath @{term"map"} leads
-to the above condition. The reason is that \isacommand{recdef} ``knows'' that @{term"map"} will
-apply @{term"trev"} only to elements of @{term"ts"}. Thus the above condition expresses that
-the size of the argument @{term"t : set ts"} of any recursive call of @{term"trev"} is strictly
-less than @{term"size(App f ts) = Suc(term_size ts)"}.
-We will now prove the termination condition and continue with our definition.
-Below we return to the question of how \isacommand{recdef} ``knows'' about @{term"map"}.
+where @{term"set"} returns the set of elements of a list (no special
+knowledge of sets is required in the following) and @{name"term_list_size ::
+term list \<Rightarrow> nat"} is an auxiliary function automatically defined by Isabelle
+(when @{name"term"} was defined).  First we have to understand why the
+recursive call of @{term"trev"} underneath @{term"map"} leads to the above
+condition. The reason is that \isacommand{recdef} ``knows'' that @{term"map"}
+will apply @{term"trev"} only to elements of @{term"ts"}. Thus the above
+condition expresses that the size of the argument @{term"t : set ts"} of any
+recursive call of @{term"trev"} is strictly less than @{term"size(App f ts) =
+Suc(term_list_size ts)"}.  We will now prove the termination condition and
+continue with our definition.  Below we return to the question of how
+\isacommand{recdef} ``knows'' about @{term"map"}.
 *};
 
 (*<*)
 end;
-(*>*)
\ No newline at end of file
+(*>*)