--- a/src/HOL/Data_Structures/AVL_Map.thy Mon Nov 16 12:37:46 2015 +0100
+++ b/src/HOL/Data_Structures/AVL_Map.thy Mon Nov 16 13:08:52 2015 +0100
@@ -38,7 +38,7 @@
interpretation Map_by_Ordered
where empty = Leaf and lookup = lookup and update = update and delete = delete
-and inorder = inorder and wf = "\<lambda>_. True"
+and inorder = inorder and inv = "\<lambda>_. True"
proof (standard, goal_cases)
case 1 show ?case by simp
next
@@ -47,6 +47,6 @@
case 3 thus ?case by(simp add: inorder_update)
next
case 4 thus ?case by(simp add: inorder_delete)
-qed (rule TrueI)+
+qed auto
end