code: private void addFieldAliases(Decl.Variable p, EnclosingScope scope) {
  		Type t = p.getType();
  		if (t instanceof Type.Record) {
  			// This is currently the only situation in which field aliases can
  			// arise.
  			Type.Record r = (Type.Record) t;
  			for (Type.Field fd : r.getFields()) {
  				scope.declareFieldAlias(fd.getName());
  			}
  		}
  	}
docs: In the special case of a record type declaration, those fields contained
  in the record are registered as "field aliases". This means they can be
  referred to directly from the type invariant, rather than requiring an
  additional variable be declared. For example, the following is permitted:
  
  <pre>
  type Point is {int x, int y} where x >= 0 && y >= 0
  </pre>
  
  Here, <code>x</code> and <code>y</code> are "field aliases" within the
  scope of the type invariant. In essence, what happens is that the above
  is silently transformed into the following:
  
  <pre>
  type Point is ({int x, int y} $) where $.x >= 0 && $.y >= 0
  </pre>
  
  The anonymous variable name <code>$</code> is chosen because it cannot
  conflict with a declared variable in the program source (i.e. it is not a
  valid variable identifier).
  
  @param p
  @param scope