# HG changeset patch
# User nipkow
# Date 1526209629 -7200
# Node ID b00f0f990bc5cd6643851b71fe4e2770a05c8a66
# Parent  057d5b4ce47e60a415e748106fcd1e8698d060aa
tuned

diff -r 057d5b4ce47e -r b00f0f990bc5 src/HOL/Data_Structures/Sorting.thy
--- a/src/HOL/Data_Structures/Sorting.thy	Sat May 12 22:20:46 2018 +0200
+++ b/src/HOL/Data_Structures/Sorting.thy	Sun May 13 13:07:09 2018 +0200
@@ -337,8 +337,7 @@
 proof (induction xs arbitrary: k m rule: c_merge_all.induct)
   case 1 thus ?case by simp
 next
-  case (2 x)
-  then show ?case by (simp)
+  case 2 thus ?case by simp
 next
   case (3 x y xs)
   let ?xs = "x # y # xs"