[isabelle-dev] Theory.get_name

[Walther Neuper]

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
-- 
------------------------------------------------------------------------
Walther Neuper                          Mailto: neuper at ist.tugraz.at
Institute for Software Technology          Tel: +43-(0)316/873-5728
University of Technology                   Fax: +43-(0)316/873-5706
Graz, Austria                             Home: www.ist.tugraz.at/neuper
------------------------------------------------------------------------