src/HOL/Data_Structures/Splay_Set.thy

--- a/src/HOL/Data_Structures/Splay_Set.thy	Thu Nov 05 11:59:45 2015 +0100
+++ b/src/HOL/Data_Structures/Splay_Set.thy	Thu Nov 05 18:38:08 2015 +0100
@@ -198,7 +198,7 @@
 
 interpretation Set_by_Ordered
 where empty = Leaf and isin = isin and insert = insert
-and delete = delete and inorder = inorder and wf = "\<lambda>_. True"
+and delete = delete and inorder = inorder and inv = "\<lambda>_. True"
 proof (standard, goal_cases)
   case 2 thus ?case by(simp add: isin_set)
 next