# HG changeset patch
# User wenzelm
# Date 1203081651 -3600
# Node ID 21b78307096f1d71ee68d6fec501c54db415396a
# Parent  321c4ca82923176c1fbf1043d2446b3a22f839df
tuned names;

diff -r 321c4ca82923 -r 21b78307096f src/Pure/Isar/isar_cmd.ML
--- 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;