--- a/src/HOL/Data_Structures/Set_Specs.thy Tue Aug 20 09:48:22 2019 +0200
+++ b/src/HOL/Data_Structures/Set_Specs.thy Tue Aug 20 12:19:23 2019 +0200
@@ -17,7 +17,7 @@
fixes invar :: "'s \<Rightarrow> bool"
assumes set_empty: "set empty = {}"
assumes set_isin: "invar s \<Longrightarrow> isin s x = (x \<in> set s)"
-assumes set_insert: "invar s \<Longrightarrow> set(insert x s) = Set.insert x (set s)"
+assumes set_insert: "invar s \<Longrightarrow> set(insert x s) = set s \<union> {x}"
assumes set_delete: "invar s \<Longrightarrow> set(delete x s) = set s - {x}"
assumes invar_empty: "invar empty"
assumes invar_insert: "invar s \<Longrightarrow> invar(insert x s)"