diff --git a/doc/lean/tutorial.org b/doc/lean/tutorial.org
index d8029a807..ecfa5499d 100644
--- a/doc/lean/tutorial.org
+++ b/doc/lean/tutorial.org
@@ -528,10 +528,12 @@ the Lean standard library.
 
 =not_intro H= produces a proof for =¬ a= from =H : a → false=. That is,
 we obtain =¬ a= if we can derive =false= from =a=. The expression
-=absurd_elim b Ha Hna= produces a proof for =b= from =Ha : a= and =Hna : ¬ a=.
+=absurd_elim Ha Hna= produces a proof for some =b= from =Ha : a= and =Hna : ¬ a=.
 That is, we can deduce anything if we have =a= and =¬ a=.
 We now use =not_intro= and =absurd_elim= to produce a proof term for
-=(a → b) → ¬b → ¬a=. =absurd Ha Hna= is just =absurd_elim false Ha Hna=.
+=(a → b) → ¬b → ¬a=. =absurd Ha Hna= is just a special case of
+=absurd_elim= where =b=
+is false.
 
 #+BEGIN_SRC lean
   import logic
@@ -560,7 +562,7 @@ Now, here is the proof term for =¬a → b → (b → a) → c=
   import logic
   variables a b c : Prop
   check fun (Hna : ¬ a) (Hb : b) (Hba : b → a),
-            absurd_elim c (Hba Hb) Hna
+            absurd_elim (Hba Hb) Hna
 #+END_SRC
 
 *** Iff (if-and-only-if)
diff --git a/library/data/bool.lean b/library/data/bool.lean
index 02bb07bd3..7091a59c0 100644
--- a/library/data/bool.lean
+++ b/library/data/bool.lean
@@ -120,7 +120,7 @@ cases_on a
 theorem band_eq_tt_elim_left {a b : bool} (H : a && b = tt) : a = tt :=
 or_elim (dichotomy a)
   (assume H0 : a = ff,
-    absurd_elim (a = tt)
+    absurd_elim
       (calc ff = ff && b : (band_ff_left _)⁻¹
            ... = a && b  : {H0⁻¹}
            ... = tt      : H)
diff --git a/library/data/int/order.lean b/library/data/int/order.lean
index d14afe778..efb406d5c 100644
--- a/library/data/int/order.lean
+++ b/library/data/int/order.lean
@@ -522,7 +522,7 @@ theorem mul_lt_cancel_left_nonneg {a b c : ℤ} (Hc : c ≥ 0) (H : c * a < c *
 or_elim (le_or_gt b a)
   (assume H2 : b ≤ a,
     have H3 : c * b ≤ c * a, from mul_le_left_nonneg Hc H2,
-    absurd_elim _ H3 (lt_imp_not_ge H))
+    absurd_elim H3 (lt_imp_not_ge H))
   (assume H2 : a < b, H2)
 
 theorem mul_lt_cancel_right_nonneg {a b c : ℤ} (Hc : c ≥ 0) (H : a * c < b * c) : a < b :=
@@ -543,7 +543,7 @@ or_elim (le_or_gt a b)
   (assume H2 : a ≤ b, H2)
   (assume H2 : a > b,
     have H3 : c * a > c * b, from mul_lt_left_pos Hc H2,
-    absurd_elim _ H3 (le_imp_not_gt H))
+    absurd_elim H3 (le_imp_not_gt H))
 
 theorem mul_le_cancel_right_pos {a b c : ℤ} (Hc : c > 0) (H : a * c ≤ b * c) : a ≤ b :=
 mul_le_cancel_left_pos Hc (subst (mul_comm b c) (subst (mul_comm a c) H))
@@ -647,7 +647,7 @@ or_elim3 (trichotomy a 0) sorry sorry sorry
 theorem to_nat_sign_ne_zero {a : ℤ} (H : a ≠ 0) : (to_nat (sign a)) = 1 :=
 or_elim3 (trichotomy a 0) sorry
 --  (by simp)
-  (assume H2 : a = 0, absurd_elim _ H2 H)
+  (assume H2 : a = 0, absurd_elim H2 H)
   sorry
 --  (by simp)
 
diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean
index 1ea3de80f..8b68a94c2 100644
--- a/library/data/list/basic.lean
+++ b/library/data/list/basic.lean
@@ -164,7 +164,7 @@ theorem head_cons (x : T) (x0 : T) (t : list T) : head x0 (x :: t) = x := refl _
 
 theorem head_concat (s t : list T) (x0 : T) : s ≠ nil → (head x0 (s ++ t) = head x0 s) :=
 list_cases_on s
-  (take H : nil ≠ nil, absurd_elim (head x0 (concat nil t) = head x0 nil) (refl nil) H)
+  (take H : nil ≠ nil, absurd_elim (refl nil) H)
   (take x s,
     take H : cons x s ≠ nil,
     calc
@@ -180,7 +180,7 @@ theorem tail_cons (x : T) (l : list T) : tail (cons x l) = l := refl _
 
 theorem cons_head_tail (x0 : T) (l : list T) : l ≠ nil → (head x0 l) :: (tail l) = l :=
 list_cases_on l
-  (assume H : nil ≠ nil, absurd_elim _ (refl _) H)
+  (assume H : nil ≠ nil, absurd_elim (refl _) H)
   (take x l, assume H : cons x l ≠ nil, refl _)
 
 
diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean
index 421f03432..4a9a1ab9f 100644
--- a/library/data/nat/basic.lean
+++ b/library/data/nat/basic.lean
@@ -255,7 +255,7 @@ induction_on n
   (take (H : 0 + m = 0), refl 0)
   (take k IH,
     assume (H : succ k + m = 0),
-    absurd_elim (succ k = 0)
+    absurd_elim
       (show succ (k + m) = 0, from
         calc
           succ (k + m) = succ k + m : symm (add_succ_left k m)
@@ -402,7 +402,7 @@ discriminate
               ... = succ k * succ l : {Hk}
               ... = k * succ l + succ l : mul_succ_left _ _
               ... = succ (k * succ l + l) : add_succ_right _ _),
-        absurd_elim _  (trans Heq H) (succ_ne_zero _)))
+        absurd_elim (trans Heq H) (succ_ne_zero _)))
 
 ---other inversion theorems appear below
 
diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean
index 87f122705..ebf56e0f3 100644
--- a/library/data/nat/order.lean
+++ b/library/data/nat/order.lean
@@ -297,7 +297,7 @@ not_succ_zero_le n
 
 theorem lt_imp_eq_succ {n m : ℕ} (H : n < m) : exists k, m = succ k :=
 discriminate
-  (take (Hm : m = 0), absurd_elim _ (subst Hm H) (not_lt_zero n))
+  (take (Hm : m = 0), absurd_elim (subst Hm H) (not_lt_zero n))
   (take (l : ℕ) (Hm : m = succ l), exists_intro l Hm)
 
 -- ### interaction with le
@@ -437,7 +437,7 @@ theorem strong_induction_on {P : nat → Prop} (n : ℕ) (H : ∀n, (∀m, m < n
 have H1 : ∀n, ∀m, m < n → P m, from
   take n,
   induction_on n
-    (show ∀m, m < 0 → P m, from take m H, absurd_elim _ H (not_lt_zero _))
+    (show ∀m, m < 0 → P m, from take m H, absurd_elim H (not_lt_zero _))
     (take n',
       assume IH : ∀m, m < n' → P m,
       have H2: P n', from H n' IH,
@@ -479,7 +479,7 @@ theorem succ_imp_pos {n m : ℕ} (H : n = succ m) : n > 0 :=
 H⁻¹ ▸ (succ_pos m)
 
 theorem ne_zero_imp_pos {n : ℕ} (H : n ≠ 0) : n > 0 :=
-or_elim (zero_or_pos n) (take H2 : n = 0, absurd_elim _ H2 H) (take H2 : n > 0, H2)
+or_elim (zero_or_pos n) (take H2 : n = 0, absurd_elim H2 H) (take H2 : n > 0, H2)
 
 theorem pos_imp_ne_zero {n : ℕ} (H : n > 0) : n ≠ 0 :=
 ne_symm (lt_imp_ne H)
@@ -512,7 +512,7 @@ discriminate
         n * m = 0 * m : {H2}
           ... = 0 : mul_zero_left m,
     have H4 : 0 > 0, from H3 ▸ H,
-    absurd_elim _ H4 (lt_irrefl 0))
+    absurd_elim H4 (lt_irrefl 0))
   (take l : nat,
     assume Hl : n = succ l,
     Hl⁻¹ ▸ (succ_pos l))
@@ -545,7 +545,7 @@ theorem mul_lt_cancel_left {n m k : ℕ} (H : k * n < k * m) : n < m :=
 or_elim (le_or_gt m n)
   (assume H2 : m ≤ n,
     have H3 : k * m ≤ k * n, from mul_le_left H2 k,
-    absurd_elim _ H3 (lt_imp_not_ge H))
+    absurd_elim H3 (lt_imp_not_ge H))
   (assume H2 : n < m, H2)
 
 theorem mul_lt_cancel_right {n m k : ℕ} (H : n * k < m * k) : n < m :=
@@ -587,7 +587,7 @@ or_elim (le_or_gt n 1)
   (assume H5 : n > 1,
     have H6 : n * m ≥ 2 * 1, from mul_le H5 H4,
     have H7 : 1 ≥ 2, from mul_one_right 2 ▸ H ▸ H6,
-    absurd_elim _ (self_lt_succ 1) (le_imp_not_gt H7))
+    absurd_elim (self_lt_succ 1) (le_imp_not_gt H7))
 
 theorem mul_eq_one_right {n m : ℕ} (H : n * m = 1) : m = 1 :=
 mul_eq_one_left ((mul_comm n m) ▸ H)
diff --git a/library/data/nat/sub.lean b/library/data/nat/sub.lean
index 1c2da2036..71cbb0bbf 100644
--- a/library/data/nat/sub.lean
+++ b/library/data/nat/sub.lean
@@ -196,7 +196,7 @@ sub_induction n m
 	... = succ (k - 0) : {symm (sub_zero_right k)})
   (take k,
     assume H : succ k ≤ 0,
-    absurd_elim _ H (not_succ_zero_le k))
+    absurd_elim H (not_succ_zero_le k))
   (take k l,
     assume IH : k ≤ l → succ l - k = succ (l - k),
     take H : succ k ≤ succ l,
@@ -215,7 +215,7 @@ sub_induction n m
     calc
       0 + (k - 0) = k - 0 : add_zero_left (k - 0)
 	... = k : sub_zero_right k)
-  (take k, assume H : succ k ≤ 0, absurd_elim _ H (not_succ_zero_le k))
+  (take k, assume H : succ k ≤ 0, absurd_elim H (not_succ_zero_le k))
   (take k l,
     assume IH : k ≤ l → k + (l - k) = l,
     take H : succ k ≤ succ l,
@@ -271,7 +271,7 @@ have l1 : k ≤ m → n + m - k = n + (m - k), from
       calc
 	n + m - 0 = n + m : sub_zero_right (n + m)
 	  ... = n + (m - 0) : {symm (sub_zero_right m)})
-    (take k : ℕ, assume H : succ k ≤ 0, absurd_elim _ H (not_succ_zero_le k))
+    (take k : ℕ, assume H : succ k ≤ 0, absurd_elim H (not_succ_zero_le k))
     (take k m,
       assume IH : k ≤ m → n + m - k = n + (m - k),
       take H : succ k ≤ succ m,
diff --git a/library/logic/axioms/classical.lean b/library/logic/axioms/classical.lean
index bb8ddcad0..ba3252205 100644
--- a/library/logic/axioms/classical.lean
+++ b/library/logic/axioms/classical.lean
@@ -98,9 +98,9 @@ eqt_intro (hrefl a)
 theorem not_or (a b : Prop) : (¬(a ∨ b)) = (¬a ∧ ¬b) :=
 propext
   (assume H, or_elim (em a)
-    (assume Ha, absurd_elim (¬a ∧ ¬b) (or_inl Ha) H)
+    (assume Ha, absurd_elim (or_inl Ha) H)
     (assume Hna, or_elim (em b)
-      (assume Hb, absurd_elim (¬a ∧ ¬b) (or_inr Hb) H)
+      (assume Hb, absurd_elim (or_inr Hb) H)
       (assume Hnb, and_intro Hna Hnb)))
   (assume (H : ¬a ∧ ¬b) (N : a ∨ b),
     or_elim N
@@ -111,7 +111,7 @@ theorem not_and (a b : Prop) : (¬(a ∧ b)) = (¬a ∨ ¬b) :=
 propext
   (assume H, or_elim (em a)
     (assume Ha, or_elim (em b)
-      (assume Hb, absurd_elim (¬a ∨ ¬b) (and_intro Ha Hb) H)
+      (assume Hb, absurd_elim (and_intro Ha Hb) H)
       (assume Hnb, or_inr Hnb))
     (assume Hna, or_inl Hna))
   (assume (H : ¬a ∨ ¬b) (N : a ∧ b),
@@ -153,7 +153,7 @@ propext (assume H, eqf_elim H) (assume H, eqf_intro H)
 
 theorem not_exists_forall {A : Type} {P : A → Prop} (H : ¬∃x, P x) : ∀x, ¬P x :=
 take x, or_elim (em (P x))
-  (assume Hp : P x,   absurd_elim (¬P x) (exists_intro x Hp) H)
+  (assume Hp : P x,   absurd_elim (exists_intro x Hp) H)
   (assume Hn : ¬P x, Hn)
 
 theorem not_forall_exists {A : Type} {P : A → Prop} (H : ¬∀x, P x) : ∃x, ¬P x :=
diff --git a/library/logic/classes/decidable.lean b/library/logic/classes/decidable.lean
index cc533b221..677d6ce53 100644
--- a/library/logic/classes/decidable.lean
+++ b/library/logic/classes/decidable.lean
@@ -27,10 +27,10 @@ theorem irrelevant {p : Prop} (d1 d2 : decidable p) : d1 = d2 :=
 decidable_rec
   (assume Hp1 : p, decidable_rec
     (assume Hp2  : p,  congr_arg inl (refl Hp1)) -- using proof irrelevance for Prop
-    (assume Hnp2 : ¬p, absurd_elim (inl Hp1 = inr Hnp2) Hp1 Hnp2)
+    (assume Hnp2 : ¬p, absurd_elim Hp1 Hnp2)
     d2)
   (assume Hnp1 : ¬p, decidable_rec
-    (assume Hp2  : p,  absurd_elim (inr Hnp1 = inl Hp2) Hp2 Hnp1)
+    (assume Hp2  : p,  absurd_elim Hp2 Hnp1)
     (assume Hnp2 : ¬p, congr_arg inr (refl Hnp1)) -- using proof irrelevance for Prop
     d2)
   d1
@@ -76,7 +76,7 @@ rec_on Ha
   (assume Hna, rec_on Hb
     (assume Hb  : b,  inr (assume H : a ↔ b, absurd (iff_elim_right H Hb) Hna))
     (assume Hnb : ¬b, inl
-        (iff_intro (assume Ha, absurd_elim b Ha Hna) (assume Hb, absurd_elim a Hb Hnb))))
+        (iff_intro (assume Ha, absurd_elim Ha Hna) (assume Hb, absurd_elim Hb Hnb))))
 
 theorem implies_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) :
   decidable (a → b) :=
@@ -84,7 +84,7 @@ rec_on Ha
   (assume Ha  : a, rec_on Hb
     (assume Hb  : b,  inl (assume H, Hb))
     (assume Hnb : ¬b, inr (assume H : a → b, absurd (H Ha) Hnb)))
-  (assume Hna : ¬a, inl (assume Ha, absurd_elim b Ha Hna))
+  (assume Hna : ¬a, inl (assume Ha, absurd_elim Ha Hna))
 
 theorem decidable_iff_equiv {a b : Prop} (Ha : decidable a) (H : a ↔ b) : decidable b :=
 rec_on Ha
diff --git a/library/logic/connectives/basic.lean b/library/logic/connectives/basic.lean
index 2669b0241..237d9aaea 100644
--- a/library/logic/connectives/basic.lean
+++ b/library/logic/connectives/basic.lean
@@ -40,7 +40,7 @@ assume Hna : ¬a, absurd Ha Hna
 theorem mt {a b : Prop} (H1 : a → b) (H2 : ¬b) : ¬a :=
 assume Ha : a, absurd (H1 Ha) H2
 
-theorem absurd_elim {a : Prop} (b : Prop) (H1 : a) (H2 : ¬a) : b :=
+theorem absurd_elim {a : Prop} {b : Prop} (H1 : a) (H2 : ¬a) : b :=
 false_elim b (absurd H1 H2)
 
 theorem absurd_not_true (H : ¬true) : false :=
@@ -50,7 +50,7 @@ theorem not_false_trivial : ¬false :=
 assume H : false, H
 
 theorem not_implies_left {a b : Prop} (H : ¬(a → b)) : ¬¬a :=
-assume Hna : ¬a, absurd (assume Ha : a, absurd_elim b Ha Hna) H
+assume Hna : ¬a, absurd (assume Ha : a, absurd_elim Ha Hna) H
 
 theorem not_implies_right {a b : Prop} (H : ¬(a → b)) : ¬b :=
 assume Hb : b, absurd (assume Ha : a, Hb) H
@@ -113,18 +113,18 @@ theorem or_elim {a b c : Prop} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c
 or_rec H2 H3 H1
 
 theorem resolve_right {a b : Prop} (H1 : a ∨ b) (H2 : ¬a) : b :=
-or_elim H1 (assume Ha, absurd_elim b Ha H2) (assume Hb, Hb)
+or_elim H1 (assume Ha, absurd_elim Ha H2) (assume Hb, Hb)
 
 theorem resolve_left {a b : Prop} (H1 : a ∨ b) (H2 : ¬b) : a :=
-or_elim H1 (assume Ha, Ha) (assume Hb, absurd_elim a Hb H2)
+or_elim H1 (assume Ha, Ha) (assume Hb, absurd_elim Hb H2)
 
 theorem or_swap {a b : Prop} (H : a ∨ b) : b ∨ a :=
 or_elim H (assume Ha, or_inr Ha) (assume Hb, or_inl Hb)
 
 theorem or_not_intro {a b : Prop} (Hna : ¬a) (Hnb : ¬b) : ¬(a ∨ b) :=
 assume H : a ∨ b, or_elim H
-  (assume Ha, absurd_elim _ Ha Hna)
-  (assume Hb, absurd_elim _ Hb Hnb)
+  (assume Ha, absurd_elim Ha Hna)
+  (assume Hb, absurd_elim Hb Hnb)
 
 theorem or_imp_or {a b c d : Prop} (H1 : a ∨ b) (H2 : a → c) (H3 : b → d) : c ∨ d :=
 or_elim H1
diff --git a/library/logic/connectives/if.lean b/library/logic/connectives/if.lean
index 4df01245d..ce655ca2b 100644
--- a/library/logic/connectives/if.lean
+++ b/library/logic/connectives/if.lean
@@ -15,12 +15,12 @@ notation `if` c `then` t `else` e:45 := ite c t e
 theorem if_pos {c : Prop} {H : decidable c} (Hc : c) {A : Type} (t e : A) : (if c then t else e) = t :=
 decidable_rec
   (assume Hc : c,    refl (@ite c (inl Hc) A t e))
-  (assume Hnc : ¬c,  absurd_elim (@ite c (inr Hnc) A t e = t) Hc Hnc)
+  (assume Hnc : ¬c,  absurd_elim Hc Hnc)
   H
 
 theorem if_neg {c : Prop} {H : decidable c} (Hnc : ¬c) {A : Type} (t e : A) : (if c then t else e) = e :=
 decidable_rec
-  (assume Hc : c,    absurd_elim (@ite c (inl Hc) A t e = e) Hc Hnc)
+  (assume Hc : c,    absurd_elim Hc Hnc)
   (assume Hnc : ¬c,  refl (@ite c (inr Hnc) A t e))
   H
 
@@ -41,9 +41,9 @@ theorem if_cond_congr {c₁ c₂ : Prop} {H₁ : decidable c₁} {H₂ : decidab
 rec_on H₁
  (assume Hc₁  : c₁,  rec_on H₂
    (assume Hc₂  : c₂,  (if_pos Hc₁ t e) ⬝ (if_pos Hc₂ t e)⁻¹)
-   (assume Hnc₂ : ¬c₂, absurd_elim _ (iff_elim_left Heq Hc₁) Hnc₂))
+   (assume Hnc₂ : ¬c₂, absurd_elim (iff_elim_left Heq Hc₁) Hnc₂))
  (assume Hnc₁ : ¬c₁, rec_on H₂
-   (assume Hc₂  : c₂,  absurd_elim _ (iff_elim_right Heq Hc₂) Hnc₁)
+   (assume Hc₂  : c₂,  absurd_elim (iff_elim_right Heq Hc₂) Hnc₁)
    (assume Hnc₂ : ¬c₂, (if_neg Hnc₁ t e) ⬝ (if_neg Hnc₂ t e)⁻¹))
 
 theorem if_congr_aux {c₁ c₂ : Prop} {H₁ : decidable c₁} {H₂ : decidable c₂} {A : Type} {t₁ t₂ e₁ e₂ : A}
diff --git a/library/logic/examples/nuprl_examples.lean b/library/logic/examples/nuprl_examples.lean
index 2ffcc896c..e5c0f299d 100644
--- a/library/logic/examples/nuprl_examples.lean
+++ b/library/logic/examples/nuprl_examples.lean
@@ -18,7 +18,7 @@ assume Hab Hbc Ha,
 -- 3. False Propositions and Negation
 theorem thm4 {P Q : Prop} : ¬P → P → Q :=
 assume Hnp Hp,
-  absurd_elim Q Hp Hnp
+  absurd_elim Hp Hnp
 
 theorem thm5 {P : Prop} : P → ¬¬P :=
 assume (Hp : P) (HnP : ¬P),
@@ -31,7 +31,7 @@ assume (Hpq : P → Q) (Hnq : ¬Q) (Hp : P),
 
 theorem thm7 {P Q : Prop} : (P → ¬P) → (P → Q) :=
 assume Hpnp Hp,
-  absurd_elim Q Hp (Hpnp Hp)
+  absurd_elim Hp (Hpnp Hp)
 
 theorem thm8 {P Q : Prop} : ¬(P → Q) → (P → ¬Q) :=
 assume (Hn : ¬(P → Q)) (Hp : P) (Hq : Q),
@@ -44,7 +44,7 @@ theorem thm9 {P : Prop} : (P ∨ ¬P) → (¬¬P → P) :=
 assume (em : P ∨ ¬P) (Hnn : ¬¬P),
   or_elim em
     (assume Hp, Hp)
-    (assume Hn, absurd_elim P Hn Hnn)
+    (assume Hn, absurd_elim Hn Hnn)
 
 theorem thm10 {P : Prop} : ¬¬(P ∨ ¬P) :=
 assume Hnem : ¬(P ∨ ¬P),
@@ -76,7 +76,7 @@ assume (H : ¬P ∧ ¬Q) (Hn : P ∨ Q),
 theorem thm14 {P Q : Prop} : ¬P ∨ Q → P → Q :=
 assume (Hor : ¬P ∨ Q) (Hp : P),
   or_elim Hor
-    (assume Hnp : ¬P, absurd_elim Q Hp Hnp)
+    (assume Hnp : ¬P, absurd_elim Hp Hnp)
     (assume Hq : Q, Hq)
 
 theorem thm15 {P Q : Prop} : (P → Q) → ¬¬(¬P ∨ Q) :=
@@ -129,7 +129,7 @@ assume (Hem : C ∨ ¬C) (Hin : ∃x : T, true) (H1 : C → ∃x, P x),
       exists_intro w Hr)
     (assume Hnc : ¬C,
       obtain (w : T) (Hw : true), from Hin,
-      have Hr : C → P w, from assume Hc, absurd_elim (P w) Hc Hnc,
+      have Hr : C → P w, from assume Hc, absurd_elim Hc Hnc,
       exists_intro w Hr)
 
 theorem thm19b : (∃x, C → P x) → C → (∃x, P x) :=
@@ -147,7 +147,7 @@ assume Hem Hin Hnf H,
       have H1 : ¬(∀x, P x), from mt H Hnc,
       have H2 : ∃x, ¬P x, from Hnf H1,
       obtain (w : T) (Hw : ¬P w), from H2,
-      exists_intro w (assume H : P w, absurd_elim C H Hw))
+      exists_intro w (assume H : P w, absurd_elim H Hw))
 
 theorem thm20b : (∃x, P x → C) → (∀ x, P x) → C :=
 assume Hex Hall,
diff --git a/tests/lean/run/class4.lean b/tests/lean/run/class4.lean
index 9ccdaaef3..2e7ecab1e 100644
--- a/tests/lean/run/class4.lean
+++ b/tests/lean/run/class4.lean
@@ -35,12 +35,12 @@ theorem is_zero_to_eq (x : nat) (H : is_zero x) : x = zero
      (assume Hz : x = zero, Hz)
      (assume Hs : (∃ n, x = succ n),
        exists_elim Hs (λ (w : nat) (Hw : x = succ w),
-         absurd_elim _ H (subst (symm Hw) (not_is_zero_succ w))))
+         absurd_elim H (subst (symm Hw) (not_is_zero_succ w))))
 
 theorem is_not_zero_to_eq {x : nat} (H : ¬ is_zero x) : ∃ n, x = succ n
 := or_elim (dichotomy x)
      (assume Hz : x = zero,
-       absurd_elim _ (subst (symm Hz) is_zero_zero) H)
+       absurd_elim (subst (symm Hz) is_zero_zero) H)
      (assume Hs, Hs)
 
 theorem not_zero_add (x y : nat) (H : ¬ is_zero y) : ¬ is_zero (x + y)
diff --git a/tests/lean/slow/nat_wo_hints.lean b/tests/lean/slow/nat_wo_hints.lean
index 9bedcedb6..2930b5549 100644
--- a/tests/lean/slow/nat_wo_hints.lean
+++ b/tests/lean/slow/nat_wo_hints.lean
@@ -228,7 +228,7 @@ theorem add_eq_zero_left {n m : ℕ} : n + m = 0 → n = 0
     (take (H : 0 + m = 0), refl 0)
     (take k IH,
       assume (H : succ k + m = 0),
-      absurd_elim (succ k = 0)
+      absurd_elim
         (show succ (k + m) = 0, from
           calc
             succ (k + m) = succ k + m : symm (add_succ_left k m)
@@ -376,7 +376,7 @@ theorem mul_eq_zero {n m : ℕ} (H : n * m = 0) : n = 0 ∨ m = 0
                 ... = succ k * succ l : { Hk }
                 ... = k * succ l + succ l : mul_succ_left _ _
                 ... = succ (k * succ l + l) : add_succ_right _ _),
-          absurd_elim _  (trans Heq H) (succ_ne_zero _)))
+          absurd_elim (trans Heq H) (succ_ne_zero _)))
 
 -- see more under "positivity" below
 -------------------------------------------------- le
@@ -694,7 +694,7 @@ theorem lt_zero_inv (n : ℕ) : ¬ n < 0
 
 theorem lt_positive {n m : ℕ} (H : n < m) : ∃k, m = succ k
 := discriminate
-    (take (Hm : m = 0), absurd_elim _ (subst Hm H) (lt_zero_inv n))
+    (take (Hm : m = 0), absurd_elim (subst Hm H) (lt_zero_inv n))
     (take (l : ℕ) (Hm : m = succ l), exists_intro l Hm)
 
 ---------- interaction with le
@@ -830,7 +830,7 @@ theorem strong_induction_on {P : ℕ → Prop} (n : ℕ) (IH : ∀n, (∀m, m <
           (take m : ℕ,
             assume H4 : m < k,
             have H5 : m < 0, from subst H2 H4,
-            absurd_elim _ H5 (lt_zero_inv m)),
+            absurd_elim H5 (lt_zero_inv m)),
         show P k, from IH k H3)
       (take l : ℕ,
         assume IHl : ∀k, k ≤ l → P k,
@@ -866,7 +866,7 @@ theorem add_eq_self {n m : ℕ} (H : n + m = n) : m = 0
             ... = n : H,
       have H3 : n < n, from lt_intro H2,
       have H4 : n ≠ n, from lt_ne H3,
-      absurd_elim _ (refl n) H4)
+      absurd_elim (refl n) H4)
 
 -------------------------------------------------- positivity
 
@@ -881,11 +881,11 @@ theorem succ_positive {n m : ℕ} (H : n = succ m) : n > 0
 := subst (symm H) (lt_zero m)
 
 theorem ne_zero_positive {n : ℕ} (H : n ≠ 0) : n > 0
-:= or_elim (zero_or_positive n) (take H2 : n = 0, absurd_elim _ H2 H) (take H2 : n > 0, H2)
+:= or_elim (zero_or_positive n) (take H2 : n = 0, absurd_elim H2 H) (take H2 : n > 0, H2)
 
 theorem pos_imp_eq_succ {n : ℕ} (H : n > 0) : ∃l, n = succ l
 := discriminate
-    (take H2, absurd_elim _ (subst H2 H) (lt_irrefl 0))
+    (take H2, absurd_elim (subst H2 H) (lt_irrefl 0))
     (take l Hl, exists_intro l Hl)
 
 theorem add_positive_right (n : ℕ) {k : ℕ} (H : k > 0) : n + k > n
@@ -918,7 +918,7 @@ theorem succ_imp_pos {n m : ℕ} (H : n = succ m) : n > 0
 := subst (symm H) (succ_pos m)
 
 theorem ne_zero_pos {n : ℕ} (H : n ≠ 0) : n > 0
-:= or_elim (zero_or_pos n) (take H2 : n = 0, absurd_elim _ H2 H) (take H2 : n > 0, H2)
+:= or_elim (zero_or_pos n) (take H2 : n = 0, absurd_elim H2 H) (take H2 : n > 0, H2)
 
 theorem add_pos_right (n : ℕ) {k : ℕ} (H : k > 0) : n + k > n
 := subst (add_zero_right n) (add_lt_left H n)
@@ -945,7 +945,7 @@ theorem mul_positive_inv_left {n m : ℕ} (H : n * m > 0) : n > 0
           n * m = 0 * m : {H2}
             ... = 0 : mul_zero_left m,
       have H4 : 0 > 0, from subst H3 H,
-      absurd_elim _ H4 (lt_irrefl 0))
+      absurd_elim H4 (lt_irrefl 0))
     (take l : ℕ,
       assume Hl : n = succ l,
       subst (symm Hl) (lt_zero l))
@@ -1061,7 +1061,7 @@ theorem mul_eq_one_left {n m : ℕ} (H : n * m = 1) : n = 1
     (assume H5 : n > 1,
       have H6 : n * m ≥ 2 * 1, from mul_le H5 H4,
       have H7 : 1 ≥ 2, from subst (mul_one_right 2) (subst H H6),
-      absurd_elim _ (self_lt_succ 1) (le_imp_not_gt H7))
+      absurd_elim (self_lt_succ 1) (le_imp_not_gt H7))
 
 theorem mul_eq_one_right {n m : ℕ} (H : n * m = 1) : m = 1
 := mul_eq_one_left (subst (mul_comm n m) H)
@@ -1222,7 +1222,7 @@ theorem succ_sub {m n : ℕ} : m ≥ n → succ m - n  = succ (m - n)
           ... = succ (k - 0) : {symm (sub_zero_right k)})
     (take k,
       assume H : succ k ≤ 0,
-      absurd_elim _ H (not_succ_zero_le k))
+      absurd_elim H (not_succ_zero_le k))
     (take k l,
       assume IH : k ≤ l → succ l - k = succ (l - k),
       take H : succ k ≤ succ l,
@@ -1241,7 +1241,7 @@ theorem add_sub_le {n m : ℕ} : n ≤ m → n + (m - n) = m
       calc
         0 + (k - 0) = k - 0 : add_zero_left (k - 0)
           ... = k : sub_zero_right k)
-    (take k, assume H : succ k ≤ 0, absurd_elim _ H (not_succ_zero_le k))
+    (take k, assume H : succ k ≤ 0, absurd_elim H (not_succ_zero_le k))
     (take k l,
       assume IH : k ≤ l → k + (l - k) = l,
       take H : succ k ≤ succ l,
@@ -1299,7 +1299,7 @@ theorem add_sub_assoc {m k : ℕ} (H : k ≤ m) (n : ℕ) : n + m - k = n + (m -
         calc
           n + m - 0 = n + m : sub_zero_right (n + m)
             ... = n + (m - 0) : {symm (sub_zero_right m)})
-      (take k : ℕ, assume H : succ k ≤ 0, absurd_elim _ H (not_succ_zero_le k))
+      (take k : ℕ, assume H : succ k ≤ 0, absurd_elim H (not_succ_zero_le k))
       (take k m,
         assume IH : k ≤ m → n + m - k = n + (m - k),
         take H : succ k ≤ succ m,