--- orig/FunctionType.java	2003-06-08 21:27:10.000000000 +0200
+++ new/FunctionType.java	2003-06-21 23:44:00.000000000 +0200
@@ -94,6 +94,11 @@
     argumentNames.add(argumentName);
   }
 
+  public void setArgumentName(int i, String name)
+  {
+    argumentNames.set(i,name);
+  }
+
   public String toString() {
     return toString(null);
   }