diff --git a/src/Lean/Meta/Tactic/Rewrites.lean b/src/Lean/Meta/Tactic/Rewrites.lean
index 68b873533d..8ebdc1af14 100644
--- a/src/Lean/Meta/Tactic/Rewrites.lean
+++ b/src/Lean/Meta/Tactic/Rewrites.lean
@@ -49,22 +49,16 @@ private def addImport (name : Name) (constInfo : ConstantInfo) :
   match name with
   | .str _ n => if n.endsWith "_inj" ∨ n.endsWith "_inj'" then return #[]
   | _ => pure ()
-  try
-    withNewMCtxDepth do withReducible do
-      forallTelescopeReducing constInfo.type fun _ type => do
-        match type.getAppFnArgs with
-        | (``Eq, #[_, lhs, rhs])
-        | (``Iff, #[lhs, rhs]) => do
-          let a := Array.mkEmpty 2
-          let a := a.push (← InitEntry.fromExpr lhs (name, RwDirection.forward))
-          let a := a.push (← InitEntry.fromExpr rhs (name, RwDirection.backward))
-          pure a
-        | _ => return #[]
-  catch _e =>
-    throwError "Jhx. Timeout initializing entries"
---      if e.isMaxHeartbeat then
---      else
---        throw e
+  withNewMCtxDepth do withReducible do
+    forallTelescopeReducing constInfo.type fun _ type => do
+      match type.getAppFnArgs with
+      | (``Eq, #[_, lhs, rhs])
+      | (``Iff, #[lhs, rhs]) => do
+        let a := Array.mkEmpty 2
+        let a := a.push (← InitEntry.fromExpr lhs (name, RwDirection.forward))
+        let a := a.push (← InitEntry.fromExpr rhs (name, RwDirection.backward))
+        pure a
+      | _ => return #[]
 
 /-- Configuration for `DiscrTree`. -/
 def discrTreeConfig : WhnfCoreConfig := {}