diff -r 2bbd945728e2 -r f14b997da756 src/HOL/Data_Structures/Set_Specs.thy
--- a/src/HOL/Data_Structures/Set_Specs.thy	Thu Aug 29 14:20:46 2019 +0200
+++ b/src/HOL/Data_Structures/Set_Specs.thy	Thu Aug 29 19:07:00 2019 +0200
@@ -66,7 +66,7 @@
   case 3 thus ?case by(simp add: inorder_insert set_ins_list set_def invar_def)
 next
   case (4 s x) thus ?case
-    by (auto simp: inorder_delete distinct_if_sorted set_del_list_eq invar_def set_def)
+    by (auto simp: inorder_delete set_del_list invar_def set_def)
 next
   case 5 thus ?case by(simp add: inorder_empty inorder_inv_empty invar_def)
 next