diff -r d122c24a93d6 -r a99a7cbf0fb5 src/HOL/Data_Structures/Sorting.thy
--- a/src/HOL/Data_Structures/Sorting.thy	Tue Oct 24 10:59:15 2017 +0200
+++ b/src/HOL/Data_Structures/Sorting.thy	Tue Oct 24 18:48:21 2017 +0200
@@ -202,6 +202,6 @@
 (* Beware of conversions: *)
 lemma "length xs = 2^k \<Longrightarrow> c_msort xs \<le> length xs * log 2 (length xs)"
 using c_msort_le[of xs k] apply (simp add: log_nat_power algebra_simps)
-by (metis (mono_tags) numeral_power_eq_real_of_nat_cancel_iff of_nat_le_iff of_nat_mult)
+by (metis (mono_tags) numeral_power_eq_of_nat_cancel_iff of_nat_le_iff of_nat_mult)
 
 end