# HG changeset patch
# User nipkow
# Date 1447414091 -3600
# Node ID f7662ca95f1b574f56fdbfadb1cd2f87fa153deb
# Parent  5121b9a57cce70983cf931628bb66e14b902a84c
tuned name

diff -r 5121b9a57cce -r f7662ca95f1b src/HOL/Data_Structures/AVL_Map.thy
--- a/src/HOL/Data_Structures/AVL_Map.thy	Fri Nov 13 12:06:50 2015 +0100
+++ b/src/HOL/Data_Structures/AVL_Map.thy	Fri Nov 13 12:28:11 2015 +0100
@@ -18,7 +18,7 @@
 fun delete :: "'a::cmp \<Rightarrow> ('a*'b) avl_tree \<Rightarrow> ('a*'b) avl_tree" where
 "delete _ Leaf = Leaf" |
 "delete x (Node h l (a,b) r) = (case cmp x a of
-   EQ \<Rightarrow> delete_root (Node h l (a,b) r) |
+   EQ \<Rightarrow> del_root (Node h l (a,b) r) |
    LT \<Rightarrow> balR (delete x l) (a,b) r |
    GT \<Rightarrow> balL l (a,b) (delete x r))"
 
@@ -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_delete_root inorder_delete_maxD split: prod.splits)
+     inorder_del_root inorder_del_maxD split: prod.splits)
 
 interpretation Map_by_Ordered
 where empty = Leaf and lookup = lookup and update = update and delete = delete