--- a/doc-src/TutorialI/Recdef/Nested1.thy Mon May 02 10:56:13 2005 +0200
+++ b/doc-src/TutorialI/Recdef/Nested1.thy Mon May 02 11:03:27 2005 +0200
@@ -26,11 +26,11 @@
and @{text"term_list_size :: term list \<Rightarrow> nat"} is an auxiliary
function automatically defined by Isabelle
(while processing the declaration of @{text term}). Why does the
-recursive call of @{term trev} lead to this
+recursive call of @{const trev} lead to this
condition? Because \isacommand{recdef} knows that @{term map}
-will apply @{term trev} only to elements of @{term ts}. Thus the
+will apply @{const trev} only to elements of @{term ts}. Thus the
condition expresses that the size of the argument @{prop"t : set ts"} of any
-recursive call of @{term trev} is strictly less than @{term"size(App f ts)"},
+recursive call of @{const trev} is strictly less than @{term"size(App f ts)"},
which equals @{term"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}.