diff -r ef1e0cb80fde -r 949d93804740 src/HOL/ex/Radix_Sort.thy
--- a/src/HOL/ex/Radix_Sort.thy	Tue May 22 14:12:15 2018 +0200
+++ b/src/HOL/ex/Radix_Sort.thy	Tue May 22 11:08:37 2018 +0200
@@ -44,7 +44,7 @@
 lemma sorted_from_Suc2:
   "\<lbrakk> cols xss n; i < n;
     sorted_col i xss;
-    \<And>x. sorted_from (i+1) [ys \<leftarrow> xss. ys!i = x] \<rbrakk>
+    \<And>x. sorted_from (i+1) (filter (\<lambda>ys. ys!i = x) xss) \<rbrakk>
   \<Longrightarrow> sorted_from i xss"
 proof(induction xss rule: induct_list012)
   case 1 show ?case by simp
@@ -68,7 +68,7 @@
   proof(rule "3.IH"[OF _ "3.prems"(2)])
     show "cols (xs2 # xss) n" using "3.prems"(1) by(simp add: cols_def)
     show "sorted_col i (xs2 # xss)" using "3.prems"(3) by simp
-    show "\<And>x. sorted_from (i+1) [ys\<leftarrow>xs2 # xss . ys ! i = x]"
+    show "\<And>x. sorted_from (i+1) (filter (\<lambda>ys. ys ! i = x) (xs2 # xss))"
       using "3.prems"(4)
         sorted_antimono_suffix[OF map_mono_suffix[OF filter_mono_suffix[OF suffix_ConsI[OF suffix_order.order.refl]]]]
       by fastforce
@@ -81,7 +81,7 @@
 shows "sorted_from i (sort_col i xss)"
 proof (rule sorted_from_Suc2[OF cols_sort1[OF assms(1)] assms(2)])
   show "sorted_col i (sort_col i xss)" by(simp add: sorted)
-  fix x show "sorted_from (i+1) [ys \<leftarrow> sort_col i xss . ys ! i = x]"
+  fix x show "sorted_from (i+1) (filter (\<lambda>ys. ys ! i = x) (sort_col i xss))"
   proof -
     from assms(3)
     have "sorted_from (i+1) (filter (\<lambda>ys. ys!i = x) xss)"