general solution to the arity bug that occasionally plagues Sledgehammer -- short story, lots of things go kaputt when a polymorphic symbol's arity in the translation is higher than the arity of the fully polymorphic HOL constant
/***************************************************************************
Title: GraphBrowser/AWTFontMetrics.java
Author: Gerwin Klein, TU Muenchen
AbstractFontMetrics avoids dependency on java.awt.FontMetrics in
batch mode.
***************************************************************************/
package GraphBrowser;
public interface AbstractFontMetrics {
public int stringWidth(String str);
public int getAscent();
public int getDescent();
}