# HG changeset patch
# User wenzelm
# Date 1222777167 -7200
# Node ID 5bad734625ef38eef751749b9778af8ae8d78d10
# Parent  25d6099179a6aab638a56b0d55092616fc946558
Toplevel.commit_exit: position;

diff -r 25d6099179a6 -r 5bad734625ef src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Sep 30 14:19:26 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Sep 30 14:19:27 2008 +0200
@@ -143,7 +143,8 @@
     val _ = name = "" andalso error ("Bad file name: " ^ quote file);
     val _ =
       if ThyInfo.check_known_thy name then
-        (Isar.>> Toplevel.commit_exit; ThyInfo.touch_child_thys name; ThyInfo.register_thy name)
+        (Isar.>> (Toplevel.commit_exit Position.none);
+            ThyInfo.touch_child_thys name; ThyInfo.register_thy name)
           handle ERROR msg =>
             (warning (cat_lines ["Failed to register theory: " ^ quote name, msg]);
               tell_file_retracted (ThyLoad.thy_path name))