diff -r 7a9118e63cad -r b0dfe57dfa09 src/HOL/Data_Structures/Sorting.thy
--- a/src/HOL/Data_Structures/Sorting.thy	Tue Sep 11 14:56:45 2018 +0200
+++ b/src/HOL/Data_Structures/Sorting.thy	Tue Sep 11 17:53:08 2018 +0200
@@ -259,7 +259,7 @@
 by (induction xs rule: merge_adj.induct) auto
 
 fun merge_all :: "('a::linorder) list list \<Rightarrow> 'a list" where
-"merge_all [] = undefined" |
+"merge_all [] = []" |
 "merge_all [xs] = xs" |
 "merge_all xss = merge_all (merge_adj xss)"