doc-src/TutorialI/Datatype/Fundata.thy

--- a/doc-src/TutorialI/Datatype/Fundata.thy	Mon Oct 09 09:33:45 2000 +0200
+++ b/doc-src/TutorialI/Datatype/Fundata.thy	Mon Oct 09 10:18:21 2000 +0200
@@ -35,7 +35,8 @@
 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, simp_all)
+apply(induct_tac T, simp_all)
+done
 
 text{*\noindent
 %apply(induct_tac T);