[isabelle-dev] Theory.get_name

[Christian Sternagel]

This can be done via 'Context.thoery_name : theory -> string'. I used 
'grep' to find this function

   $ grep -R 'val' /usr/local/Isabelle/src/ | grep ':' | \
     grep 'string$' | grep theory | less

I.e., i searched in all of Isabelle sources for some function signature 
(starting with 'val' and containing a ':' before the type) who's result 
type (assuming that this is written at the end of the line) is 'string' 
and there is also 'theory' contained somewhere. I always build these 
piped greps incrementally until I no longer get to many results.

It's very easy to find functions this way.

cheers

chris

On 08/19/2009 08:57 PM, Walther Neuper wrote:
> Hi all,
>
> migrating code based on a _very_ old version of Isabelle to
> Isabelle2009, I'm happy with the many improvements.
>
> Our code switches between object-language (e.g.theory, thm) and
> meta-language (i.e.string) and thus we need
>
> ML> Thm.get_name;
> val it = fn : Thm.thm -> string
>
> but there is no Theory.get_name ;-( In the old Isabelle version the
> following worked fine:
>
> fun string_of_thy thy = ((last_elem (Sign.stamp_names_of (sign_of
> thy)))^".thy"):theory';
>
> How could that be achieved in Isabelle2009 ?
>
> Many thanks in advance,
> Walther