# HG changeset patch
# User wenzelm
# Date 1160415426 -7200
# Node ID 2a39f21257729d8023a095d79904d4c560c04e35
# Parent  b2f67b947200c3d161e3a2131c7ae3b1a0656039
Secure.commit;

diff -r b2f67b947200 -r 2a39f2125772 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Mon Oct 09 19:37:05 2006 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Mon Oct 09 19:37:06 2006 +0200
@@ -179,8 +179,7 @@
 fun use_mltext v txt = Toplevel.keep' (fn verb => fn state =>
   (Context.use_mltext txt (v andalso verb) (try Toplevel.theory_of state)));
 
-(*commit is dynamically bound!*)
-val use_commit = use_mltext false "commit();";
+val use_commit = Toplevel.imperative Secure.commit;
 
 
 (* current working directory *)