use_mltext: priority output;
authorwenzelm
Fri, 12 Jan 2001 20:04:22 +0100
changeset 10893 408906dd1e1b
parent 10892 405b077433a3
child 10894 ce58d2de6ea8
use_mltext: priority output;
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;