diff -r 2f5edb146f7e -r 1f073030b97a doc-src/TutorialI/Overview/RECDEF.thy
--- a/doc-src/TutorialI/Overview/RECDEF.thy	Fri Jan 18 17:46:17 2002 +0100
+++ b/doc-src/TutorialI/Overview/RECDEF.thy	Fri Jan 18 18:30:19 2002 +0100
@@ -73,7 +73,7 @@
 
 lemma "mirror(mirror t) = t"
 apply(induct_tac t rule: mirror.induct)
-apply(simp add:rev_map sym[OF map_compose] cong:map_cong)
+apply(simp add: rev_map sym[OF map_compose] cong: map_cong)
 done
 
 text{*