# HG changeset patch
# User wenzelm
# Date 939836532 -7200
# Node ID fe7b7e3c3ddc773f08464fc1bfe58f3fac8d1d59
# Parent  a4acf1b4d5a8d8ed43e790203b2a53a5621aa50c
use_text_verbose;

diff -r a4acf1b4d5a8 -r fe7b7e3c3ddc src/Pure/Thy/thm_database.ML
--- a/src/Pure/Thy/thm_database.ML	Wed Oct 13 19:41:35 1999 +0200
+++ b/src/Pure/Thy/thm_database.ML	Wed Oct 13 19:42:12 1999 +0200
@@ -68,16 +68,18 @@
   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;
+
 fun ml_store_thm (name, thm) =
   let val thm' = store_thm (name, thm) in
     if warn_ml name then ()
-    else (qed_thms := [thm']; use_text true ("val " ^ name ^ " = hd (! ThmDatabase.qed_thms);"))
+    else (qed_thms := [thm']; use_text_verbose ("val " ^ name ^ " = hd (! ThmDatabase.qed_thms);"))
   end;
 
 fun ml_store_thms (name, thms) =
   let val thms' = store_thms (name, thms) in
     if warn_ml name then ()
-    else (qed_thms := thms'; use_text true ("val " ^ name ^ " = ! ThmDatabase.qed_thms;"))
+    else (qed_thms := thms'; use_text_verbose ("val " ^ name ^ " = ! ThmDatabase.qed_thms;"))
   end;
 
 fun bind_thm (name, thm) = ml_store_thm (name, standard thm);