diff -r 1b7a901e2edc -r 90d03908b3d7 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Jul 20 11:47:17 2009 +0200
+++ b/src/HOL/Set.thy	Mon Jul 20 15:24:15 2009 +0200
@@ -589,7 +589,7 @@
   by blast
 
 lemma equals0D: "A = {} ==> a \<notin> A"
-    -- {* Use for reasoning about disjointness: @{prop "A Int B = {}"} *}
+    -- {* Use for reasoning about disjointness: @{text "A Int B = {}"} *}
   by blast
 
 lemma ball_empty [simp]: "Ball {} P = True"