doc-src/TutorialI/Datatype/Fundata.thy

--- a/doc-src/TutorialI/Datatype/Fundata.thy	Fri Aug 25 12:17:09 2000 +0200
+++ b/doc-src/TutorialI/Datatype/Fundata.thy	Mon Aug 28 09:32:51 2000 +0200
@@ -36,7 +36,7 @@
 The following lemma has a canonical proof  *}
 
 lemma "map_bt (g o f) T = map_bt g (map_bt f T)";
-by(induct_tac "T", auto)
+by(induct_tac "T", simp_all)
 
 text{*\noindent
 but it is worth taking a look at the proof state after the induction step