| changeset 39910 | 10097e0a9dbd |
| parent 39246 | 9e58f0499f57 |
| child 40825 | c55ee3793712 |
--- a/src/HOL/Induct/QuoDataType.thy Fri Oct 01 14:15:49 2010 +0200 +++ b/src/HOL/Induct/QuoDataType.thy Fri Oct 01 16:05:25 2010 +0200 @@ -422,7 +422,7 @@ 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)