--- a/src/HOL/ex/Radix_Sort.thy Wed Feb 21 12:57:49 2018 +0000
+++ b/src/HOL/ex/Radix_Sort.thy Thu Feb 22 19:48:01 2018 +0100
@@ -56,7 +56,7 @@
lemma sorted_from_radix_sort_step:
"\<lbrakk> cols xss n; i < n; sorted_from (Suc i) xss \<rbrakk> \<Longrightarrow> sorted_from i (sort_key (\<lambda>xs. xs ! i) xss)"
apply (rule sorted_from_Suc2)
-apply (auto simp add: sort_key_stable[of _ xss "%xs. xs!i"] sorted_filter cols_def)
+apply (auto simp add: sort_key_stable sorted_filter cols_def)
done
lemma sorted_from_radix_sort: