On Thu, 23 Sep 2010, Walther Neuper wrote:
we have hundreds of tests on very old code relying on a function
term2str = fn : term -> string, with: term2str @{term "str"} = "str"
i.e., the string _without_ markup.
ML {*
fun term2str trm = Syntax.string_of_term (ProofContext.init_global
(theory "Isac")) trm;
The standard way to do that is via the wrapper Print_Mode.setmp [] -- as
can be glimpsed from various existing examples in the sources.
Further notes on contemporary Isabelle/ML coding style:
* "term2str" is non-conventional, use term_to_string or string_of_term
or similar;
* "trm" is non-conventional, even though the Urban tutorial claims it
is, use t or tm or similar;
* function "theory" is very old style, use @{theory} antiquotation.
Makarius
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
