Angst angst angst! Programming is hard. Twelf is a big ball of stuff. I am afraid I will have to change the interface to substitution inversion. Also, adding a new parameter to a huge mound of mutually recusive functions which is simply passed along in the common case is hard, but it seems like it ought to be made easy somehow. Hmm.