diff --git a/library/tools/super/simp.lean b/library/tools/super/simp.lean
index 582c618ceb..ec296a7a18 100644
--- a/library/tools/super/simp.lean
+++ b/library/tools/super/simp.lean
@@ -35,7 +35,6 @@ on_right_at' c i $ λhyp, do
   prf  ← mk_app ``eq.mpr [heqsymm, hyp],
   return [(add_hyps, prf)]
 
-@[super.inf]
 meta def simp_inf : inf_decl := inf_decl.mk 40 $ take given, sequence' $ do
 r ← [try_simplify_right, try_simplify_left],
 i ← list.range given^.c^.num_lits,
diff --git a/tests/lean/run/super_examples.lean b/tests/lean/run/super_examples.lean
index 9e59b3b4d3..f438cb45f3 100644
--- a/tests/lean/run/super_examples.lean
+++ b/tests/lean/run/super_examples.lean
@@ -23,11 +23,10 @@ example (n : ℕ) : n > 0 ↔ is_positive n := by super
 example (m n : ℕ) : 0 + m = 0 + n → m = n :=
 by super with nat.zero_add
 
-local attribute [simp] nat.zero_add nat.succ_add
-@[simp] lemma nat_add_succ (m n : ℕ) : m + nat.succ n = nat.succ (m + n) := rfl
-@[simp] lemma nat_zero_has_zero : nat.zero = 0 := rfl
 example : ∀x y : ℕ, x + y = y + x :=
-begin intros, induction x, super, super end
+begin intros, induction x,
+      super with nat.add_zero nat.zero_add,
+      super with nat.add_succ nat.succ_add end
 
 example (i) [inhabited i] : nonempty i := by super
 example (i) [nonempty i] : ¬(inhabited i → false) := by super