[isabelle-dev] fun : term -> string

[Makarius]

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