--- a/NEWS Thu Oct 16 23:56:57 2008 +0200
+++ b/NEWS Thu Oct 16 23:58:29 2008 +0200
@@ -52,7 +52,7 @@
covered by the constraints in the initial statement, completed by the
type instance information of the background theory. Non-trivial sort
hypotheses, which rarely occur in practice, may be specified via
-vacuous propositions of the form SORT_CONSTRAIN('a::c). For example:
+vacuous propositions of the form SORT_CONSTRAINT('a::c). For example:
lemma assumes "SORT_CONSTRAINT('a::empty)" shows False ...