diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index f7f50dade5..82c56b9177 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -266,7 +266,7 @@ where
     | [] => return s
     | fvarId::todo =>
       if s.contains fvarId then
-        return s
+        loop todo s
       else
         let (todo, s) ← visit fvarId todo <| s.insert fvarId
         loop todo s
diff --git a/tests/lean/run/inductionAltExplicit.lean b/tests/lean/run/inductionAltExplicit.lean
index 36faa871ee..1235523a84 100644
--- a/tests/lean/run/inductionAltExplicit.lean
+++ b/tests/lean/run/inductionAltExplicit.lean
@@ -11,8 +11,8 @@ def lexAccessible1 {ra : α → α → Prop} {rb : β → β → Prop} (aca : (a
       apply Acc.intro (xa, xb)
       intro p lt
       cases lt with
-      | left  b1 b2 h    => apply iha _ h _ (aca _ h)
-      | @right a b1 b2 h => apply ihb _ h (acb _ h)
+      | left  b1 b2 h    => apply iha _ h
+      | @right a b1 b2 h => apply ihb _ h
 
 def lexAccessible2 {ra : α → α → Prop} {rb : β → β → Prop} (aca : (a : α) → Acc ra a) (acb : (b : β) → Acc rb b) (a : α) (b : β) : Acc (Lex ra rb) (a, b) := by
   induction (aca a) generalizing b with
@@ -22,5 +22,5 @@ def lexAccessible2 {ra : α → α → Prop} {rb : β → β → Prop} (aca : (a
       apply Acc.intro (xa, xb)
       intro p lt
       cases lt with
-      | @left a1 b1 a2 b2 h => apply iha _ h _ (aca _ h)
-      | right _ h           => apply ihb _ h (acb _ h)
+      | @left a1 b1 a2 b2 h => apply iha _ h
+      | right _ h           => apply ihb _ h