diff -r d40cc6e7bfd8 -r aea72a834c85 doc-src/TutorialI/Inductive/AB.thy
--- a/doc-src/TutorialI/Inductive/AB.thy	Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/Inductive/AB.thy	Thu Nov 29 21:12:37 2001 +0100
@@ -132,7 +132,7 @@
 discuss it.
 *}
 
-apply(induct w)
+apply(induct_tac w)
  apply(simp)
 by(force simp add: zabs_def take_Cons split: nat.split if_splits)