# HG changeset patch
# User wenzelm
# Date 939836423 -7200
# Node ID 4a6df182b09386a12a79f9e6df58a930c81689a1
# Parent  3689adcf9b8bef4c7892f0336aeb5f28123f878d
use_text writeln;

diff -r 3689adcf9b8b -r 4a6df182b093 src/Pure/Isar/isar_thy.ML
--- 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;