Strange. The proof worked in the 2008 release. In order to make it work now, the last line of the proof must be moved up two places. In other words, the first proof step is now returning its subgoals in a different order from before.

Name.binding

added optimizer

reactivated some dead theories (based on hints by Mark Hillebrand);

Locale.local_note_qualified

fact table now using name bindings

dropped legacy naming code

tuned name bindings

using name bindings

name spaces and name bindings