--- 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