diff -r ff9e9d5ac171 -r 10097e0a9dbd src/HOL/Induct/QuoNestedDataType.thy
--- a/src/HOL/Induct/QuoNestedDataType.thy	Fri Oct 01 14:15:49 2010 +0200
+++ b/src/HOL/Induct/QuoNestedDataType.thy	Fri Oct 01 16:05:25 2010 +0200
@@ -337,7 +337,7 @@
 
 definition
   "fun" :: "exp \<Rightarrow> nat" where
-  "fun X = contents (\<Union>U \<in> Rep_Exp X. {freefun U})"
+  "fun X = the_elem (\<Union>U \<in> Rep_Exp X. {freefun U})"
 
 lemma fun_respects: "(%U. {freefun U}) respects exprel"
 by (simp add: congruent_def exprel_imp_eq_freefun) 
@@ -349,7 +349,7 @@
 
 definition
   args :: "exp \<Rightarrow> exp list" where
-  "args X = contents (\<Union>U \<in> Rep_Exp X. {Abs_ExpList (freeargs U)})"
+  "args X = the_elem (\<Union>U \<in> Rep_Exp X. {Abs_ExpList (freeargs U)})"
 
 text{*This result can probably be generalized to arbitrary equivalence
 relations, but with little benefit here.*}
@@ -384,7 +384,7 @@
 
 definition
   discrim :: "exp \<Rightarrow> int" where
-  "discrim X = contents (\<Union>U \<in> Rep_Exp X. {freediscrim U})"
+  "discrim X = the_elem (\<Union>U \<in> Rep_Exp X. {freediscrim U})"
 
 lemma discrim_respects: "(\<lambda>U. {freediscrim U}) respects exprel"
 by (simp add: congruent_def exprel_imp_eq_freediscrim)