--- a/src/HOL/Library/DAList.thy Thu Feb 16 22:18:28 2012 +0100
+++ b/src/HOL/Library/DAList.thy Thu Feb 16 22:53:24 2012 +0100
@@ -12,8 +12,10 @@
subsection {* Type @{text "('key, 'value) alist" } *}
typedef (open) ('key, 'value) alist = "{xs :: ('key \<times> 'value) list. distinct (map fst xs)}"
-morphisms impl_of Alist
-by(rule exI[where x="[]"]) simp
+ morphisms impl_of Alist
+proof
+ show "[] \<in> {xs. distinct (map fst xs)}" by simp
+qed
lemma alist_ext: "impl_of xs = impl_of ys \<Longrightarrow> xs = ys"
by(simp add: impl_of_inject)