diff -r 4939494ed791 -r ce654b0e6d69 src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/Library/While_Combinator.thy	Thu Feb 15 12:11:00 2018 +0100
@@ -387,7 +387,7 @@
 qualified fun rtrancl_while_invariant :: "'a list \<times> 'a set \<Rightarrow> bool"
 where "rtrancl_while_invariant (ws, Z) =
    (x \<in> Z \<and> set ws \<subseteq> Z \<and> distinct ws \<and> {(x,y). y \<in> set(f x)} `` (Z - set ws) \<subseteq> Z \<and>
-    Z \<subseteq> {(x,y). y \<in> set(f x)}^* `` {x} \<and> (\<forall>z\<in>Z - set ws. p z))"
+    Z \<subseteq> {(x,y). y \<in> set(f x)}\<^sup>* `` {x} \<and> (\<forall>z\<in>Z - set ws. p z))"
 
 qualified lemma rtrancl_while_invariant: 
   assumes inv: "rtrancl_while_invariant st" and test: "rtrancl_while_test st"
@@ -400,8 +400,8 @@
 
 lemma rtrancl_while_Some: assumes "rtrancl_while = Some(ws,Z)"
 shows "if ws = []
-       then Z = {(x,y). y \<in> set(f x)}^* `` {x} \<and> (\<forall>z\<in>Z. p z)
-       else \<not>p(hd ws) \<and> hd ws \<in> {(x,y). y \<in> set(f x)}^* `` {x}"
+       then Z = {(x,y). y \<in> set(f x)}\<^sup>* `` {x} \<and> (\<forall>z\<in>Z. p z)
+       else \<not>p(hd ws) \<and> hd ws \<in> {(x,y). y \<in> set(f x)}\<^sup>* `` {x}"
 proof -
   have "rtrancl_while_invariant ([x],{x})" by simp
   with rtrancl_while_invariant have I: "rtrancl_while_invariant (ws,Z)"