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 ------------------------------------------------------------------------
