# HG changeset patch
# User wenzelm
# Date 979326281 -3600
# Node ID ce58d2de6ea8487b2f1cf8100589f032c1d2e1af
# Parent  408906dd1e1b51436dd130122d3ce28cdf961448
use_text_verbose: priority output;

diff -r 408906dd1e1b -r ce58d2de6ea8 src/Pure/Thy/thm_database.ML
--- a/src/Pure/Thy/thm_database.ML	Fri Jan 12 20:04:22 2001 +0100
+++ b/src/Pure/Thy/thm_database.ML	Fri Jan 12 20:04:41 2001 +0100
@@ -68,7 +68,7 @@
   else if name = "" then true
   else (warning ("Cannot bind theorem(s) " ^ quote name ^ " as ML value"); true);
 
-val use_text_verbose = use_text writeln true;
+val use_text_verbose = use_text priority true;
 
 fun ml_store_thm (name, thm) =
   let val thm' = store_thm (name, thm) in