diff --git a/tests/lean/noncomp_theory.lean.expected.out b/tests/lean/noncomp_theory.lean.expected.out
index 03fea7cda..dfa6026e4 100644
--- a/tests/lean/noncomp_theory.lean.expected.out
+++ b/tests/lean/noncomp_theory.lean.expected.out
@@ -1,4 +1,4 @@
-noncomp_theory.lean:4:0: error: definition 'f' is noncomputable, it depends on 'real.real_has_div'
+noncomp_theory.lean:4:0: error: definition 'f' is noncomputable, it depends on 'real.discrete_linear_ordered_field'
 noncomputable definition g : ℝ → ℝ → ℝ :=
 λ (a : ℝ), div (a + a)
 definition r : ℕ → ℕ :=
diff --git a/tests/lean/simplifier_light.lean b/tests/lean/simplifier_light.lean
index 4fcc5922b..c27c58734 100644
--- a/tests/lean/simplifier_light.lean
+++ b/tests/lean/simplifier_light.lean
@@ -40,10 +40,10 @@ namespace s
 open set
 universe l
 constants (A : Type.{l}) (x y z v w : set A)
-attribute complement [light 2]
+attribute compl [light 2]
 
 -- TODO(dhs, leo): Where do we put this group of simp rules?
-attribute union_comp_self [simp]
+attribute union_compl_self [simp]
 lemma union_comp_self_left [simp] {X : Type} (s t : set X) : s ∪ (-s ∪ t)= univ := sorry
 
 attribute union_comm [simp]
@@ -52,8 +52,8 @@ 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_compl_self [simp]
+lemma inter_compl_self_left [simp] {X : Type} (s t : set X) : s ∩ (-s ∩ t)= empty := sorry
 
 attribute inter_comm [simp]
 attribute inter_assoc [simp]