--- a/src/Pure/Isar/isar_cmd.ML Thu Feb 14 21:33:44 2008 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Fri Feb 15 14:20:51 2008 +0100
@@ -383,8 +383,8 @@
val use_mltext_theory = Toplevel.theory' o (Context.theory_map oo ML_Context.use_mltext_update);
(*ignore result theory context*)
-fun use_mltext v txt = Toplevel.keep' (fn verb => fn state =>
- (ML_Context.use_mltext txt (v andalso verb) (try Toplevel.generic_theory_of state)));
+fun use_mltext verbose txt = Toplevel.keep' (fn int => fn state =>
+ (ML_Context.use_mltext txt (verbose andalso int) (try Toplevel.generic_theory_of state)));
val use_commit = Toplevel.imperative Secure.commit;