src/HOL/Library/Countable.thy
changeset 39302 d7728f65b353
parent 39250 548a3e5521ab
child 40702 cf26dd7395e4
--- a/src/HOL/Library/Countable.thy	Mon Sep 13 08:43:48 2010 +0200
+++ b/src/HOL/Library/Countable.thy	Mon Sep 13 11:13:15 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 ext_iff)
+      by (rule injI, simp add: xs fun_eq_iff)
   qed
 qed