diff --git a/library/init/meta/injection_tactic.lean b/library/init/meta/injection_tactic.lean
index d71af54cb9..562766b4ee 100644
--- a/library/init/meta/injection_tactic.lean
+++ b/library/init/meta/injection_tactic.lean
@@ -20,20 +20,21 @@ private meta_definition injection_intro : expr → list name → tactic unit
   Hname ← return $ mk_intro_name n ns,
   H ← intro Hname,
   Ht ← infer_type H,
-  try $
-    -- Clear new hypothesis if it is of the form (a = a)
-    do { (lhs, rhs) ← match_eq Ht,
-          unify lhs rhs, clear H }
-    <|>
-    -- If new hypothesis is of the form (@heq A a B b) where
-    -- A and B can be unified then convert it into (a = b) using
-    -- the eq_of_heq lemma
-    do { (A, lhs, B, rhs) ← match_heq Ht,
-         unify A B,
-         Heq ← mk_app "eq" [lhs, rhs],
-         pr  ← mk_app "eq_of_heq" [H],
-         assertv Hname Heq pr,
-         clear H },
+  -- Clear new hypothesis if it is of the form (a = a)
+  try $ do {
+    (lhs, rhs) ← match_eq Ht,
+    unify lhs rhs,
+    clear H },
+  -- If new hypothesis is of the form (@heq A a B b) where
+  -- A and B can be unified then convert it into (a = b) using
+  -- the eq_of_heq lemma
+  try $ do {
+    (A, lhs, B, rhs) ← match_heq Ht,
+    unify A B,
+    Heq ← mk_app "eq" [lhs, rhs],
+    pr  ← mk_app "eq_of_heq" [H],
+    assertv Hname Heq pr,
+    clear H },
   injection_intro d (tail ns)
 | e  ns           := skip