src/HOL/Library/Countable.thy
changeset 39198 f967a16dfcdd
parent 37715 44b27ea94a16
child 39250 548a3e5521ab
--- a/src/HOL/Library/Countable.thy	Mon Sep 06 22:58:06 2010 +0200
+++ b/src/HOL/Library/Countable.thy	Tue Sep 07 10:05:19 2010 +0200
@@ -139,7 +139,7 @@
   show "\<exists>to_nat::('a \<Rightarrow> 'b) \<Rightarrow> nat. inj to_nat"
   proof
     show "inj (\<lambda>f. to_nat (map f xs))"
-      by (rule injI, simp add: xs expand_fun_eq)
+      by (rule injI, simp add: xs ext_iff)
   qed
 qed