diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_Monad.ml b/ocaml/fstar-lib/generated/FStar_Tactics_Monad.ml
index da21b844d4b..0c96d1be061 100644
--- a/ocaml/fstar-lib/generated/FStar_Tactics_Monad.ml
+++ b/ocaml/fstar-lib/generated/FStar_Tactics_Monad.ml
@@ -318,6 +318,9 @@ let catch : 'a . 'a tac -> (Prims.exn, 'a) FStar_Pervasives.either tac =
   fun t ->
     mk_tac
       (fun ps ->
+         let idtable =
+           FStar_Compiler_Effect.op_Bang
+             (ps.FStar_Tactics_Types.main_context).FStar_TypeChecker_Env.identifier_info in
          let tx = FStar_Syntax_Unionfind.new_transaction () in
          let uu___ = run t ps in
          match uu___ with
@@ -326,6 +329,9 @@ let catch : 'a . 'a tac -> (Prims.exn, 'a) FStar_Pervasives.either tac =
               FStar_Tactics_Result.Success ((FStar_Pervasives.Inr a1), q))
          | FStar_Tactics_Result.Failed (m, q) ->
              (FStar_Syntax_Unionfind.rollback tx;
+              FStar_Compiler_Effect.op_Colon_Equals
+                (ps.FStar_Tactics_Types.main_context).FStar_TypeChecker_Env.identifier_info
+                idtable;
               (let ps1 =
                  {
                    FStar_Tactics_Types.main_context =
diff --git a/src/tactics/FStar.Tactics.Monad.fst b/src/tactics/FStar.Tactics.Monad.fst
index a7b2d9afbb0..55f37e55ef7 100644
--- a/src/tactics/FStar.Tactics.Monad.fst
+++ b/src/tactics/FStar.Tactics.Monad.fst
@@ -169,6 +169,7 @@ let fail msg = fail_doc [text msg]
 
 let catch (t : tac 'a) : tac (either exn 'a) =
     mk_tac (fun ps ->
+            let idtable = !ps.main_context.identifier_info in
             let tx = UF.new_transaction () in
             match run t ps with
             | Success (a, q) ->
@@ -176,6 +177,7 @@ let catch (t : tac 'a) : tac (either exn 'a) =
                 Success (Inr a, q)
             | Failed (m, q) ->
                 UF.rollback tx;
+                ps.main_context.identifier_info := idtable;
                 let ps = { ps with freshness = q.freshness } in //propagate the freshness even on failures
                 Success (Inl m, ps)
            )