diff -r ff9e9d5ac171 -r 10097e0a9dbd src/HOL/Set.thy
--- a/src/HOL/Set.thy	Fri Oct 01 14:15:49 2010 +0200
+++ b/src/HOL/Set.thy	Fri Oct 01 16:05:25 2010 +0200
@@ -1656,11 +1656,11 @@
 
 subsubsection {* Getting the Contents of a Singleton Set *}
 
-definition contents :: "'a set \<Rightarrow> 'a" where
-  "contents X = (THE x. X = {x})"
+definition the_elem :: "'a set \<Rightarrow> 'a" where
+  "the_elem X = (THE x. X = {x})"
 
-lemma contents_eq [simp]: "contents {x} = x"
-  by (simp add: contents_def)
+lemma the_elem_eq [simp]: "the_elem {x} = x"
+  by (simp add: the_elem_def)
 
 
 subsubsection {* Least value operator *}