diff -r 17909568216e -r f7c1f585edeb src/HOL/Data_Structures/Set_Specs.thy
--- 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)"