src/Pure/ProofGeneral/proof_general_emacs.ML
changeset 25436 ca46d8a66b69
parent 25192 b568f8c5d5ca
child 25442 0337e3df3187
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Nov 15 11:49:03 2007 +0100
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Nov 15 11:49:04 2007 +0100
@@ -166,7 +166,7 @@
 
 (* get informed about files *)
 
-val thy_name = Path.implode o #1 o Path.split_ext o Path.base o Path.explode;
+val thy_name = perhaps (try (unsuffix ".thy")) o List.last o space_explode "/";
 
 val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
 val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;