diff --git a/library/data/finset/basic.lean b/library/data/finset/basic.lean
index dac9fd4dc..3446676f6 100644
--- a/library/data/finset/basic.lean
+++ b/library/data/finset/basic.lean
@@ -145,7 +145,7 @@ quot.lift_on s
 
 -- set builder notation
 notation `{[`:max a:(foldr `,` (x b, insert x b) ∅) `]}`:0 := a
-notation `⦃` a:(foldr `,` (x b, insert x b) ∅) `⦄` := a
+-- notation `⦃` a:(foldr `,` (x b, insert x b) ∅) `⦄` := a
 
 theorem mem_insert (a : A) (s : finset A) : a ∈ insert a s :=
 quot.induction_on s
@@ -165,7 +165,7 @@ propext (iff.intro
     (assume H' : x = a, eq.subst (eq.symm H') !mem_insert)
     (assume H' : x ∈ s, !mem_insert_of_mem H')))
 
-theorem insert_empty_eq (a : A) : ⦃a⦄ = singleton a := rfl
+theorem insert_empty_eq (a : A) : {[ a ]} = singleton a := rfl
 
 theorem insert_eq_of_mem {a : A} {s : finset A} (H : a ∈ s) : insert a s = s :=
 ext
@@ -306,7 +306,7 @@ ext (take x,
     x ∈ insert a s ↔ x ∈ insert a s            : iff.refl
                ... = (x = a ∨ x ∈ s)           : mem_insert_eq
                ... = (x ∈ singleton a ∨ x ∈ s) : mem_singleton_eq
-               ... = (x ∈ ⦃a⦄ ∪ s)             : mem_union_eq)
+               ... = (x ∈ {[ a ]} ∪ s)         : mem_union_eq)
 
 theorem insert_union (a : A) (s t : finset A) : insert a (s ∪ t) = insert a s ∪ t :=
 by rewrite [*insert_eq, union.assoc]
diff --git a/library/data/set/basic.lean b/library/data/set/basic.lean
index 6c276dc43..4cf2d7104 100644
--- a/library/data/set/basic.lean
+++ b/library/data/set/basic.lean
@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.set.basic
 Author: Jeremy Avigad, Leonardo de Moura
 -/
 import logic
@@ -126,10 +124,9 @@ notation `{` binders `|` r:(scoped:1 P, set_of P) `}` := r
 definition filter (P : X → Prop) (s : set X) : set X := λx, x ∈ s ∧ P x
 notation `{` binders ∈ s `|` r:(scoped:1 p, filter p s) `}` := r
 
--- {[x, y, z]} or ⦃x, y, z⦄
+-- {[x, y, z]}
 definition insert (x : X) (a : set X) : set X := {y : X | y = x ∨ y ∈ a}
 notation `{[`:max a:(foldr `,` (x b, insert x b) ∅) `]}`:0 := a
-notation `⦃` a:(foldr `,` (x b, insert x b) ∅) `⦄` := a
 
 /- set difference -/