diff -r d5ff8b782b29 -r fee7cfa69c50 src/Doc/Tutorial/Misc/Tree2.thy
--- a/src/Doc/Tutorial/Misc/Tree2.thy	Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Misc/Tree2.thy	Sat Nov 01 14:20:38 2014 +0100
@@ -16,7 +16,7 @@
 (*<*)
 lemma [simp]: "!xs. flatten2 t xs = flatten t @ xs"
 apply(induct_tac t)
-by(auto);
+by(auto)
 (*>*)
 lemma "flatten2 t [] = flatten t"
 (*<*)