diff -r 4939494ed791 -r ce654b0e6d69 src/HOL/Library/Countable_Set.thy
--- a/src/HOL/Library/Countable_Set.thy	Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/Library/Countable_Set.thy	Thu Feb 15 12:11:00 2018 +0100
@@ -266,7 +266,7 @@
 by(induction n)(simp_all add: assms)
 
 lemma countable_rtrancl:
-  "(\<And>Y. countable Y \<Longrightarrow> countable (X `` Y)) \<Longrightarrow> countable Y \<Longrightarrow> countable (X^* `` Y)"
+  "(\<And>Y. countable Y \<Longrightarrow> countable (X `` Y)) \<Longrightarrow> countable Y \<Longrightarrow> countable (X\<^sup>* `` Y)"
   unfolding rtrancl_is_UN_relpow UN_Image by (intro countable_UN countableI_type countable_relpow)
 
 lemma countable_lists[intro, simp]: