diff -r 308e74afab83 -r 8d0c2d74ad63 src/HOL/Library/Countable_Set.thy
--- 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