diff --git a/tests/lean/axioms_of.lean b/tests/lean/axioms_of.lean
index 2ff97f522..9adad7a53 100644
--- a/tests/lean/axioms_of.lean
+++ b/tests/lean/axioms_of.lean
@@ -10,4 +10,4 @@ print axioms finset.union
 print "-----"
 print axioms finset.mem
 print "-----"
-print axioms finset.union.comm
+print axioms finset.union_comm
diff --git a/tests/lean/simplifier_light.lean b/tests/lean/simplifier_light.lean
index 703f8ea14..4fcc5922b 100644
--- a/tests/lean/simplifier_light.lean
+++ b/tests/lean/simplifier_light.lean
@@ -46,18 +46,18 @@ attribute complement [light 2]
 attribute union_comp_self [simp]
 lemma union_comp_self_left [simp] {X : Type} (s t : set X) : s ∪ (-s ∪ t)= univ := sorry
 
-attribute union.comm [simp]
-attribute union.assoc [simp]
-attribute union.left_comm [simp]
+attribute union_comm [simp]
+attribute union_assoc [simp]
+attribute union_left_comm [simp]
 
 #simplify eq env 0 x ∪ y ∪ z ∪ -x
 
 attribute inter_comp_self [simp]
 lemma inter_comp_self_left [simp] {X : Type} (s t : set X) : s ∩ (-s ∩ t)= empty := sorry
 
-attribute inter.comm [simp]
-attribute inter.assoc [simp]
-attribute inter.left_comm [simp]
+attribute inter_comm [simp]
+attribute inter_assoc [simp]
+attribute inter_left_comm [simp]
 
 #simplify eq env 0 x ∩ y ∩ z ∩ -x