--- a/src/HOL/Data_Structures/Tree_Set.thy Wed Jun 13 11:53:25 2018 +0200
+++ b/src/HOL/Data_Structures/Tree_Set.thy Wed Jun 13 15:24:20 2018 +0200
@@ -62,7 +62,7 @@
"sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
by(induction t) (auto simp: del_list_simps split_minD split: prod.splits)
-interpretation Set_by_Ordered
+interpretation S: Set_by_Ordered
where empty = empty and isin = isin and insert = insert and delete = delete
and inorder = inorder and inv = "\<lambda>_. True"
proof (standard, goal_cases)