diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index e0c316e1a9..ab798efe33 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -453,7 +453,7 @@ do
    (e, newvars, locals) ← do {
       none ← pure rec_name | pure (e, [], []),
       t ← infer_type e,
-      -- TODO(Kha): `t ← whnf_ginductive t,`
+      t ← whnf_ginductive t,
       const n _ ← pure t.get_app_fn | pure (e, [], []),
       env ← get_env,
       tt ← pure $ env.is_inductive n | pure (e, [], []),