src/HOL/Induct/QuoDataType.thy

 text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't
 need this function in order to prove discrimination theorems.*}
 
 definition
   discrim :: "msg \<Rightarrow> int" where
-   "discrim X = contents (\<Union>U \<in> Rep_Msg X. {freediscrim U})"
+   "discrim X = the_elem (\<Union>U \<in> Rep_Msg X. {freediscrim U})"
 
 lemma discrim_congruent: "(\<lambda>U. {freediscrim U}) respects msgrel"
 by (simp add: congruent_def msgrel_imp_eq_freediscrim) 
 
 text{*Now prove the four equations for @{term discrim}*}