Josef: >Again, mostly - here is a quick counterexample. Try uncommenting the >commented def in following, and see how the parsing changes: [...] Ouch! So I have always thought the Mizar term parser to be different from this. So thanks for showing this example. Freek