src/HOL/Data_Structures/Sorting.thy

 text \<open>For the termination proof of \<open>merge_all\<close> below.\<close>
 lemma length_merge_adjacent[simp]: "length (merge_adj xs) = (length xs + 1) div 2"
 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)"
 
 definition msort_bu :: "('a::linorder) list \<Rightarrow> 'a list" where
 "msort_bu xs = (if xs = [] then [] else merge_all (map (\<lambda>x. [x]) xs))"