diff --git a/src/Lean/Meta/Tactic/Grind/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Internalize.lean
index 35222cdf58..3969f8d733 100644
--- a/src/Lean/Meta/Tactic/Grind/Internalize.lean
+++ b/src/Lean/Meta/Tactic/Grind/Internalize.lean
@@ -380,7 +380,13 @@ where
     trace_goal[grind.internalize] "[{generation}] {e}"
     match e with
     | .bvar .. => unreachable!
-    | .sort .. => return ()
+    | .sort .. =>
+      /-
+      **Note**: It may seem wasteful to create ENodes for sorts, but it is useful for the E-matching module.
+      The E-matching module assumes that the arguments of an internalized application have also been internalized,
+      unless they are `grind` gadgets.
+      -/
+      mkENode' e generation
     | .fvar .. =>
       mkENode' e generation
       checkAndAddSplitCandidate e
diff --git a/tests/lean/run/grind_sort_intern.lean b/tests/lean/run/grind_sort_intern.lean
new file mode 100644
index 0000000000..81536bc2f1
--- /dev/null
+++ b/tests/lean/run/grind_sort_intern.lean
@@ -0,0 +1,16 @@
+def f (α : Sort u) (_ : α) : Nat := 0
+
+theorem feq : f (List α) x = 0 := rfl
+
+/--
+error: `grind` failed
+case grind
+h : ¬f Prop True = 0
+⊢ False
+-/
+#guard_msgs in
+example: f Prop True = 0 := by
+  grind -verbose [feq] -- must not produce error `Prop` has not been internalized
+
+example: f Prop True = 0 := by
+  grind [f]