src/Pure/Isar/isar_cmd.ML
changeset 20927 2a39f2125772
parent 20803 ac78eee049ce
child 20957 f2a795db0500
--- 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 *)