diff --git a/src/library/tactic/induction_tactic.cpp b/src/library/tactic/induction_tactic.cpp
index 70ebb9b311..995f4b820e 100644
--- a/src/library/tactic/induction_tactic.cpp
+++ b/src/library/tactic/induction_tactic.cpp
@@ -332,11 +332,16 @@ public:
                             // last one
                             return execute(g, H, H_type, r);
                         } else {
+                            list<name>     saved_ids   = m_ids;
+                            constraint_seq saved_cs    = m_cs;
+                            substitution   saved_subst = m_subst;
                             try {
-                                flet<list<name>>     save_ids(m_ids, m_ids);
-                                flet<constraint_seq> save_cs(m_cs, m_cs);
                                 return execute(g, H, H_type, r);
-                            } catch (exception &) {}
+                            } catch (exception &) {
+                                m_ids   = saved_ids;
+                                m_cs    = saved_cs;
+                                m_subst = saved_subst;
+                            }
                         }
                     }
                 }
diff --git a/tests/lean/hott/892.hlean b/tests/lean/hott/892.hlean
new file mode 100644
index 0000000000..706f998901
--- /dev/null
+++ b/tests/lean/hott/892.hlean
@@ -0,0 +1,13 @@
+open is_trunc unit
+
+protected definition trunc.elim {n : trunc_index} {A : Type} {P : Type}
+  [Pt : is_trunc n P] (H : A → P) : trunc n A → P :=
+trunc.rec H
+
+attribute trunc.rec  [recursor 6]
+attribute trunc.elim [recursor 6]
+
+example (x : trunc -1 unit) : unit :=
+begin
+  induction x, exact star
+end