--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Sun Jul 25 12:57:29 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Sun Jul 25 14:41:48 2010 +0200
@@ -138,8 +138,8 @@
val _ = name = "" andalso error ("Bad file name: " ^ quote file);
val _ =
if Thy_Info.known_thy name then
- (Isar.>> (Toplevel.commit_exit Position.none);
- Thy_Info.touch_child_thys name; Thy_Info.register_thy name)
+ (Thy_Info.register_thy name (Toplevel.end_theory Position.none (Isar.state ()));
+ Thy_Info.touch_child_thys name)
handle ERROR msg =>
(warning (cat_lines ["Failed to register theory: " ^ quote name, msg]);
tell_file_retracted (Thy_Header.thy_path name))