# HG changeset patch
# User wenzelm
# Date 979326262 -3600
# Node ID 408906dd1e1b51436dd130122d3ce28cdf961448
# Parent  405b077433a3a129b35f5b78a92b673fe8e09547
use_mltext: priority output;

diff -r 405b077433a3 -r 408906dd1e1b src/Pure/context.ML
--- a/src/Pure/context.ML	Fri Jan 12 20:04:00 2001 +0100
+++ b/src/Pure/context.ML	Fri Jan 12 20:04:22 2001 +0100
@@ -69,8 +69,8 @@
 
 (* use ML text *)
 
-fun use_mltext txt verb opt_thy = setmp opt_thy (fn () => use_text writeln verb txt) ();
-fun use_mltext_theory txt verb thy = #2 (pass_theory thy (use_text writeln verb) txt);
+fun use_mltext txt verb opt_thy = setmp opt_thy (fn () => use_text priority verb txt) ();
+fun use_mltext_theory txt verb thy = #2 (pass_theory thy (use_text priority verb) txt);
 
 fun use_context txt = use_mltext_theory ("Context.>> (" ^ txt ^ ");") false;