diff -r 4dc65845eab3 -r d8d7d1b785af doc-src/TutorialI/Sets/Examples.thy
--- a/doc-src/TutorialI/Sets/Examples.thy	Wed Feb 24 11:55:52 2010 +0100
+++ b/doc-src/TutorialI/Sets/Examples.thy	Mon Mar 01 13:40:23 2010 +0100
@@ -156,8 +156,7 @@
 lemma "{x. P x \<longrightarrow> Q x} = -{x. P x} \<union> {x. Q x}"
 by blast
 
-constdefs
-  prime   :: "nat set"
+definition prime :: "nat set" where
     "prime == {p. 1<p & (ALL m. m dvd p --> m=1 | m=p)}"
 
 lemma "{p*q | p q. p\<in>prime \<and> q\<in>prime} =