The answer to "How can I generate a proof article file from a HOL Light theory file?" at http://www.gilith.com/software/opentheory/faq.html doesn't mention the function "export_thm". Should it? (I can't get HOL Light to build at the moment, else I would have just tried following the steps to see.)