# HG changeset patch
# User nipkow
# Date 1536697500 -7200
# Node ID 96b15934a17af343bd5b384b87562275e100f3a1
# Parent  938f4058c07c4766f10ab12c2a2f8224f6a4f7ed
tuned proof

diff -r 938f4058c07c -r 96b15934a17a src/HOL/Data_Structures/Sorting.thy
--- a/src/HOL/Data_Structures/Sorting.thy	Tue Sep 11 18:12:11 2018 +0200
+++ b/src/HOL/Data_Structures/Sorting.thy	Tue Sep 11 22:25:00 2018 +0200
@@ -333,9 +333,9 @@
   let ?xss2 = "merge_adj ?xss"
   obtain k' where k': "k = Suc k'" using "3.prems"(2)
     by (metis length_Cons nat.inject nat_power_eq_Suc_0_iff nat.exhaust)
-  have "even (length xss)" using "3.prems"(2) even_Suc_Suc_iff by fastforce
-  from "3.prems"(1) length_merge_adj[OF this]
-  have *: "\<forall>x \<in> set(merge_adj ?xss). length x = 2*m" by(auto simp: length_merge)
+  have "even (length ?xss)" using "3.prems"(2) k' by auto
+  from length_merge_adj[OF this "3.prems"(1)]
+  have *: "\<forall>x \<in> set(merge_adj ?xss). length x = 2*m" .
   have **: "length ?xss2 = 2 ^ k'" using "3.prems"(2) k' by auto
   have "c_merge_all ?xss = c_merge_adj ?xss + c_merge_all ?xss2" by simp
   also have "\<dots> \<le> m * 2^k + c_merge_all ?xss2"