<div dir="ltr">Hello,<div><br></div><div>I wish to write an ML function that does the following: transform the name of a fact to (Facts.ref * Token.src list) such that it can be used as part of Sledgehammer_Fact.fact_override.</div><div><br></div><div>The requirement arises from the need to translate the command e.g., "sledgehammer (del: one_add_one)" in Isabelle/jEdit to Isabelle/ML. I only have the name of the fact but not its proper representation for Sledgehammer fact_override. I tried to look at what the parser does but cannot decipher its behaviour. Therefore I would greatly appreciate a succinct function that does the transformation specified above.</div><div><br></div><div>Many thanks,</div><div>Albert</div></div>