lib/browser/GraphBrowser/ParseError.java

renamed (hardly used) 'prod_pred' and 'option_pred' to 'pred_prod' and 'pred_option'

package GraphBrowser;

class ParseError extends Exception {
	public ParseError(String s) { super(s); }
}