This paper presents an improvement of Herbrand’s theorem. We propose a method for specifying a sub-universe of the Herbrand universe of a clause set $ {\mathcal{S}} $, the number of ground instances may decrease considerably in many cases. We present an algorithm for automatically deriving the sub-universes for arguments in a given clause set, and show the correctness of our improvement. Moreover, we introduce an application of our approach to model generation theorem proving for non-range-restricted problems, show the range-restriction transformation algorithm based on our improvement and provide examples on benchmark problems to demonstrate the power of our approach.