Suppose I do gaussian process regression and calculate the log likelihood of observing the samples $y$ as:
$$ \log\, p(y | x, \theta_{\Sigma}, \theta_{\mu}) = - \frac{1}{2} \mathrm{log}\, \lvert\Sigma\rvert - \frac{1}{2} (y-\mu)^{T} \Sigma^{-1}(y-\mu) -\frac{n}{2}\mathrm{log}(2\pi). $$
I.e., this is the classical log marginal likelihood but with some modeled $\mu(x, \theta_{\mu})$. Is it formally correct to call $\mathrm{log}\, p(y | x, \theta_{\Sigma}, \theta_{\mu})$ the marginal likelihood? I ask because I thought this property is called "marginal" since the modeling of a mean function $f$ is "marginalized" out (which is true for most cases).
According to Gaussian Processes for Machine Learning (GPML), the log marginal likelihood is not the distribution you gave, but instead $ \log p(\mathbf{y} \mid X) $ with the mean & covariance parameters marginalized out (like you thought it should be). We compute the marginal likelihood by integrating over the parameters, $$ p(\mathbf{y} \mid X) = \int p(\mathbf{y} \mid \mathbf{f}, X) p(\mathbf{f} \mid X) d\mathbf{f}. $$
In GPML, the term you gave that includes specific parameter values is instead just called the likelihood, similar to the likelihood of a standard distribution $$ \mathcal{L}(X, \theta) = p(X, \theta) \propto P(X \mid \theta). $$