diff -r f6c40213675b -r ddc3b72f9a42 src/Pure/ProofGeneral/proof_general_emacs.ML
--- 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))