--- a/src/HOL/Data_Structures/Tree_Map.thy Thu Nov 12 21:12:09 2015 +0100
+++ b/src/HOL/Data_Structures/Tree_Map.thy Fri Nov 13 12:06:50 2015 +0100
@@ -44,7 +44,7 @@
"del_min t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> sorted1(inorder t) \<Longrightarrow>
x # inorder t' = inorder t"
by(induction t arbitrary: t' rule: del_min.induct)
- (auto simp: del_list_simps split: prod.splits)
+ (auto simp: del_list_simps split: prod.splits if_splits)
lemma inorder_delete:
"sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"