src/HOL/Data_Structures/Sorting.thy

--- a/src/HOL/Data_Structures/Sorting.thy	Wed Jun 03 11:44:21 2020 +0200
+++ b/src/HOL/Data_Structures/Sorting.thy	Thu Jun 04 15:30:22 2020 +0000
@@ -205,7 +205,8 @@
 lemma length_msort: "length(msort xs) = length xs"
 proof (induction xs rule: msort.induct)
   case (1 xs)
-  thus ?case by (auto simp: msort.simps[of xs] length_merge)
+  show ?case
+    by (auto simp: msort.simps [of xs] 1 length_merge)
 qed
 text \<open>Why structured proof?
    To have the name "xs" to specialize msort.simps with xs