# HG changeset patch
# User nipkow
# Date 1536681188 -7200
# Node ID b0dfe57dfa09d42f1f37ecb12002c551e491e68f
# Parent  7a9118e63cad2f5515d6478aa7da3c6c563150a0
"undefined" not needed, [] is perfectly natural

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)"