Before revision: As an example, the fact that the identity function can have any type of the form A → A would be formalized in System F as the judgment where is a type variable.
After revision: As an example, the fact that the identity function can have any type of the form A → A would be formalized in System F as the where is a type variable.