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 *)