src/HOL/Induct/QuoDataType.thy
changeset 39910 10097e0a9dbd
parent 39246 9e58f0499f57
child 40825 c55ee3793712
     1.1 --- a/src/HOL/Induct/QuoDataType.thy	Fri Oct 01 14:15:49 2010 +0200
     1.2 +++ b/src/HOL/Induct/QuoDataType.thy	Fri Oct 01 16:05:25 2010 +0200
     1.3 @@ -422,7 +422,7 @@
     1.4  
     1.5  definition
     1.6    discrim :: "msg \<Rightarrow> int" where
     1.7 -   "discrim X = contents (\<Union>U \<in> Rep_Msg X. {freediscrim U})"
     1.8 +   "discrim X = the_elem (\<Union>U \<in> Rep_Msg X. {freediscrim U})"
     1.9  
    1.10  lemma discrim_congruent: "(\<lambda>U. {freediscrim U}) respects msgrel"
    1.11  by (simp add: congruent_def msgrel_imp_eq_freediscrim)