diff -r c3974cd2d381 -r 1d2907d0ed73 src/HOL/Data_Structures/Tree23_Set.thy
--- a/src/HOL/Data_Structures/Tree23_Set.thy	Thu Nov 05 11:59:45 2015 +0100
+++ b/src/HOL/Data_Structures/Tree23_Set.thy	Thu Nov 05 18:38:08 2015 +0100
@@ -356,7 +356,7 @@
 
 interpretation Set_by_Ordered
 where empty = Leaf and isin = isin and insert = insert and delete = delete
-and inorder = inorder and wf = bal
+and inorder = inorder and inv = bal
 proof (standard, goal_cases)
   case 2 thus ?case by(simp add: isin_set)
 next