diff --git a/library/init/lean/elaborator.lean b/library/init/lean/elaborator.lean
index f90b548d0b..12dda551a8 100644
--- a/library/init/lean/elaborator.lean
+++ b/library/init/lean/elaborator.lean
@@ -650,13 +650,11 @@ do
       cmd ← current_command,
       some n ← pure cmd.as_node |
         error cmd $ "not a command: " ++ to_string cmd,
-      -- TODO(Sebastian): throw error on unknown command when we get serious
-      some elab ← pure $ elaborators.find n.kind.name |
-        -- TODO(Sebastian): reuse `log_message`
-        modify $ λ st, {st with messages := st.messages.add {filename := "foo", pos := ⟨1,0⟩, text := "unknown command: " ++ to_string n.kind.name}},
-        -- error cmd $ "unknown command: " ++ to_string n.kind.name,
-      catch elab $ λ e,
-        modify $ λ st, {st with messages := st.messages.add e})
+      catch
+        (do some elab ← pure $ elaborators.find n.kind.name |
+              error cmd $ "unknown command: " ++ to_string n.kind.name,
+            elab)
+        (λ e, modify $ λ st, {st with messages := st.messages.add e}))
     elaborator.max_recursion,
   match p with
   | except.ok ((), st) := pure st.messages