--- a/src/HOL/Library/Countable_Set.thy Mon Sep 20 13:51:32 2021 +0200
+++ b/src/HOL/Library/Countable_Set.thy Mon Sep 20 13:52:09 2021 +0200
@@ -377,7 +377,8 @@
lemma infinite_countable_subset':
assumes X: "infinite X" shows "\<exists>C\<subseteq>X. countable C \<and> infinite C"
proof -
- from infinite_countable_subset[OF X] guess f ..
+ obtain f :: "nat \<Rightarrow> 'a" where "inj f" "range f \<subseteq> X"
+ using infinite_countable_subset [OF X] by blast
then show ?thesis
by (intro exI[of _ "range f"]) (auto simp: range_inj_infinite)
qed