val theory2domID = string_of_thy;

 val theory2domID = string_of_thy;

 val theory2thyID = (get_thy o string_of_thy) : theory -> thyID;

 val theory2thyID = (get_thy o string_of_thy) : theory -> thyID;

 val theory2theory' = string_of_thy;

 val theory2theory' = string_of_thy;

 val theory2str = string_of_thy; (*WN050903 ..most consistent naming*)

 val theory2str = string_of_thy; (*WN050903 ..most consistent naming*)

 val theory2str' = implode o (drop_last_n 4) o explode o string_of_thy;

 val theory2str' = implode o (drop_last_n 4) o explode o string_of_thy;

 al it = "Isac" : string

 al it = "Isac" : string

 *)

 *)

 fun thyID2theory' (thyID:thyID) =

 fun thyID2theory' (thyID:thyID) =

     let val ss = explode thyID

     let val ss = explode thyID

 	val ext = implode (takelast (4, ss))

 	val ext = implode (takelast (4, ss))

     in if ext = ".thy" then thyID : theory' (*disarm abuse of thyID*)

     in if ext = ".thy" then thyID : theory' (*disarm abuse of thyID*)

        else thyID ^ ".thy"

        else thyID ^ ".thy"

     end;

     end;

 (* thyID2theory' "Isac" (*ok*);

 (* thyID2theory' "Isac" (*ok*);

 *)

 *)

 fun theory'2thyID (theory':theory') =

 fun theory'2thyID (theory':theory') =

     let val ss = explode theory'

     let val ss = explode theory'

 	val ext = implode (takelast (4, ss))

 	val ext = implode (takelast (4, ss))

     in if ext = ".thy" then ((implode o (drop_last_n 4)) ss) : thyID

     in if ext = ".thy" then ((implode o (drop_last_n 4)) ss) : thyID

        else theory' (*disarm abuse of theory'*)

        else theory' (*disarm abuse of theory'*)

     end;

     end;

 val it = "Isac" : thyID

 val it = "Isac" : thyID

 > theory'2thyID "Isac";

 > theory'2thyID "Isac";

 val it = "Isac" : thyID*)

 val it = "Isac" : thyID*)