We present a new approach to implement graphical user interfaces (GUIs) for theorem provers and formal development support tools. A typed interface between Standard ML and Tcl/Tk provides the foundations, upon which a generic GUI is built. Besides the advantage of type safeness, this technique yields access to the full power of the modularisation concepts of Standard ML: the generic GUI is a functor (a parametric module), which instantiated with a particular application yields a GUI for this application. We present a prototypical implementation with two instantiations: an interface to Isabelle itself and a system for transformational program development based on Isabelle.