--- a/src/HOL/Data_Structures/Tree_Map.thy Mon Nov 16 12:37:46 2015 +0100
+++ b/src/HOL/Data_Structures/Tree_Map.thy Mon Nov 16 13:08:52 2015 +0100
@@ -44,7 +44,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
@@ -53,6 +53,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