--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Tue Jul 31 00:56:31 2007 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Tue Jul 31 00:56:32 2007 +0200
@@ -169,7 +169,7 @@
let val name = thy_name file in
if ThyInfo.known_thy name then
(ThyInfo.touch_child_thys name;
- ThyInfo.pretend_use_thy_only name handle ERROR msg =>
+ ThyInfo.register_thy name handle ERROR msg =>
(warning (cat_lines [msg, "Failed to register theory: " ^ quote name]);
tell_file_retracted (Path.base (Path.explode file))))
else raise Toplevel.UNDEF
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Tue Jul 31 00:56:31 2007 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Tue Jul 31 00:56:32 2007 +0200
@@ -356,7 +356,7 @@
let val name = thy_name path in
if Toplevel.is_toplevel state andalso ThyInfo.known_thy name then
(ThyInfo.touch_child_thys name;
- ThyInfo.pretend_use_thy_only name handle ERROR msg =>
+ ThyInfo.register_thy name handle ERROR msg =>
(warning (cat_lines [msg, "Failed to register theory: " ^ quote name]);
tell_file_retracted true (Path.base path)))
else raise Toplevel.UNDEF