--- a/src/HOL/Data_Structures/AVL_Map.thy Sun Apr 22 21:05:14 2018 +0100
+++ b/src/HOL/Data_Structures/AVL_Map.thy Mon Apr 23 08:09:50 2018 +0200
@@ -34,7 +34,7 @@
"sorted1(inorder t) \<Longrightarrow> inorder (delete x t) = del_list x (inorder t)"
by(induction t)
(auto simp: del_list_simps inorder_balL inorder_balR
- inorder_del_root inorder_del_maxD split: prod.splits)
+ inorder_del_root inorder_split_maxD split: prod.splits)
interpretation Map_by_Ordered
where empty = Leaf and lookup = lookup and update = update and delete = delete