diff -r d40cc6e7bfd8 -r aea72a834c85 doc-src/TutorialI/Recdef/document/termination.tex
--- a/doc-src/TutorialI/Recdef/document/termination.tex	Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/Recdef/document/termination.tex	Thu Nov 29 21:12:37 2001 +0100
@@ -24,12 +24,10 @@
 \ \ {\isachardoublequote}f{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymle}\ y\ then\ x\ else\ f{\isacharparenleft}x{\isacharcomma}y{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
 %
 \begin{isamarkuptext}%
-\noindent
-Isabelle prints a
-\REMARK{error or warning?  change this part?  rename g to f?}
-message showing you what it was unable to prove. You will then
-have to prove it as a separate lemma before you attempt the definition
-of your function once more. In our case the required lemma is the obvious one:%
+\noindent This definition fails, and Isabelle prints an error message
+showing you what it was unable to prove. You will then have to prove it as a
+separate lemma before you attempt the definition of your function once
+more. In our case the required lemma is the obvious one:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{lemma}\ termi{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequote}{\isasymnot}\ x\ {\isasymle}\ y\ {\isasymLongrightarrow}\ x\ {\isacharminus}\ Suc\ y\ {\isacharless}\ x\ {\isacharminus}\ y{\isachardoublequote}\isamarkupfalse%
@@ -48,24 +46,24 @@
 \noindent
 Because \isacommand{recdef}'s termination prover involves simplification,
 we include in our second attempt a hint: the \attrdx{recdef_simp} attribute 
-says to use \isa{termi{\isacharunderscore}lem} as
-a simplification rule.%
+says to use \isa{termi{\isacharunderscore}lem} as a simplification rule.%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{consts}\ g\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
+\isamarkupfalse%
 \isamarkupfalse%
-\isacommand{recdef}\ g\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharminus}y{\isacharparenright}{\isachardoublequote}\isanewline
-\ \ {\isachardoublequote}g{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymle}\ y\ then\ x\ else\ g{\isacharparenleft}x{\isacharcomma}y{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{recdef}\ f\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharminus}y{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}f{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymle}\ y\ then\ x\ else\ f{\isacharparenleft}x{\isacharcomma}y{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}simp{\isacharcolon}\ termi{\isacharunderscore}lem{\isacharparenright}\isamarkupfalse%
+\isamarkupfalse%
 %
 \begin{isamarkuptext}%
 \noindent
-This time everything works fine. Now \isa{g{\isachardot}simps} contains precisely
-the stated recursion equation for \isa{g}, which has been stored as a
+This time everything works fine. Now \isa{f{\isachardot}simps} contains precisely
+the stated recursion equation for \isa{{\isacharquery}{\isacharquery}{\isachardot}f}, which has been stored as a
 simplification rule.  Thus we can automatically prove results such as this one:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{theorem}\ {\isachardoublequote}g{\isacharparenleft}{\isadigit{1}}{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ g{\isacharparenleft}{\isadigit{1}}{\isacharcomma}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
+\isacommand{theorem}\ {\isachardoublequote}f{\isacharparenleft}{\isadigit{1}}{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ f{\isacharparenleft}{\isadigit{1}}{\isacharcomma}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
 \isamarkupfalse%
 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
 \isamarkupfalse%
@@ -78,22 +76,7 @@
 If the termination proof requires a new lemma that is of general use, you can
 turn it permanently into a simplification rule, in which case the above
 \isacommand{hint} is not necessary. But our \isa{termi{\isacharunderscore}lem} is not
-sufficiently general to warrant this distinction.
-
-The attentive reader may wonder why we chose to call our function \isa{g}
-rather than \isa{f} the second time around. The reason is that, despite
-the failed termination proof, the definition of \isa{f} did not
-fail, and thus we could not define it a second time. However, all theorems
-about \isa{f}, for example \isa{f{\isachardot}simps}, carry as a precondition
-the unproved termination condition. Moreover, the theorems
-\isa{f{\isachardot}simps} are not stored as simplification rules. 
-However, this mechanism
-allows a delayed proof of termination: instead of proving
-\isa{termi{\isacharunderscore}lem} up front, we could prove 
-it later on and then use it to remove the preconditions from the theorems
-about \isa{f}. In most cases this is more cumbersome than proving things
-up front.
-\REMARK{FIXME, with one exception: nested recursion.}%
+sufficiently general to warrant this distinction.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isamarkupfalse%