[isabelle-dev] fun : term -> string

[Walther Neuper]

On 09/23/2010 04:03 PM, Makarius wrote:
> [...]
> The standard way to do that is via the wrapper Print_Mode.setmp [] -- 
> as can be glimpsed from various existing examples in the sources.

Thank you for the hint above, and also for the notes below (now these 
are just in time ;-)
>
> 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
>
Walther