Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use_text_verbose: priority output;
authorwenzelm
Fri, 12 Jan 2001 20:04:41 +0100
changeset 10894 ce58d2de6ea8
parent 10893 408906dd1e1b
child 10895 79194f07d356
use_text_verbose: priority output;
src/Pure/Thy/thm_database.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle