--- a/Paper/document/root.tex	Fri Mar 19 18:56:13 2010 +0100
+++ b/Paper/document/root.tex	Fri Mar 19 21:04:24 2010 +0100
@@ -49,8 +49,8 @@
 prover. It provides a proving infrastructure for convenient reasoning about
 programming language calculi involving bound variables that have names (as
 opposed to de-Bruijn indices). In this paper we present an extension of
-Nominal Isabelle for dealing with general binding structures, that means
-where multiple variables are bound at once. Such
+Nominal Isabelle for dealing with general bindings, that means
+term-constructors where multiple variables are bound at once. Such
 binding structures are ubiquitous in programming language research and only
 very poorly supported with single binders, such as the lambdas in the
 lambda-calculus. Our extension includes novel definitions of