diff -r 55c0f9a8df78 -r 59961d32b1ae doc-src/TutorialI/Sets/Functions.thy
--- a/doc-src/TutorialI/Sets/Functions.thy	Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/Sets/Functions.thy	Fri Jan 26 15:50:28 2001 +0100
@@ -79,7 +79,7 @@
 *}
 
 lemma "inj f \<Longrightarrow> (f o g = f o h) = (g = h)";
-  apply (simp add: expand_fun_eq inj_on_def o_def)
+  apply (simp add: expand_fun_eq inj_on_def)
   apply (auto)
   done