--- a/src/Pure/Isar/isar_thy.ML Wed Oct 13 19:40:03 1999 +0200
+++ b/src/Pure/Isar/isar_thy.ML Wed Oct 13 19:40:23 1999 +0200
@@ -457,11 +457,10 @@
(Obtain.obtain_i (map Comment.ignore xs) (map Comment.ignore asms));
-
(* use ML text *)
-fun use_mltext txt verb opt_thy = Context.setmp opt_thy (use_text verb) txt;
-fun use_mltext_theory txt verb thy = #2 (Context.pass_theory thy (use_text verb) txt);
+fun use_mltext txt verb opt_thy = Context.setmp opt_thy (use_text writeln verb) txt;
+fun use_mltext_theory txt verb thy = #2 (Context.pass_theory thy (use_text writeln verb) txt);
fun use_context txt = use_mltext_theory ("Context.>> (" ^ txt ^ ");") false;