diff -r 5a4d78204492 -r 7c4ec77a8715 doc-src/TutorialI/Inductive/Even.thy
--- a/doc-src/TutorialI/Inductive/Even.thy	Thu Nov 29 13:33:45 2001 +0100
+++ b/doc-src/TutorialI/Inductive/Even.thy	Thu Nov 29 14:12:42 2001 +0100
@@ -21,7 +21,7 @@
 
 Our first lemma states that numbers of the form $2\times k$ are even. *}
 lemma two_times_even[intro!]: "2*k \<in> even"
-apply (induct "k")
+apply (induct_tac k)
 txt{*
 The first step is induction on the natural number \isa{k}, which leaves
 two subgoals: