diff -r cc8aa63bdad6 -r 8016321c7de1 doc-src/TutorialI/Misc/prime_def.thy
--- a/doc-src/TutorialI/Misc/prime_def.thy	Tue Sep 05 13:12:00 2000 +0200
+++ b/doc-src/TutorialI/Misc/prime_def.thy	Tue Sep 05 13:53:39 2000 +0200
@@ -2,17 +2,18 @@
 theory prime_def = Main:;
 consts prime :: "nat \\<Rightarrow> bool"
 (*>*)
-(*<*)term(*>*)
-
-    "prime(p) \\<equiv> 1 < p \\<and> (m dvd p \\<longrightarrow> (m=1 \\<or> m=p))";
-text{*\noindent\small
+text{*
+\begin{warn}
+A common mistake when writing definitions is to introduce extra free
+variables on the right-hand side as in the following fictitious definition:
+@{term[display,quotes]"prime(p) == 1 < p & (m dvd p --> (m=1 | m=p))"}
 where @{text"dvd"} means ``divides''.
 Isabelle rejects this ``definition'' because of the extra @{term"m"} on the
 right-hand side, which would introduce an inconsistency (why?). What you
 should have written is
+@{term[display,quotes]"prime(p) == 1 < p & (!m. m dvd p --> (m=1 | m=p))"}
+\end{warn}
 *}
-(*<*)term(*>*)
- "prime(p) \\<equiv> 1 < p \\<and> (\\<forall>m. m dvd p \\<longrightarrow> (m=1 \\<or> m=p))"
 (*<*)
 end
 (*>*)