Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Thy/thm_database.ML
changeset 1580 e3fd931e6095
parent 1512 ce37c64244c0
child 1654 faa643c33ee6 
--- a/src/Pure/Thy/thm_database.ML	Thu Mar 14 16:40:18 1996 +0100
+++ b/src/Pure/Thy/thm_database.ML	Fri Mar 15 12:01:19 1996 +0100
@@ -86,7 +86,7 @@
             end;
 
       val const_idx' = update_db false consts const_idx;
-  in if consts = [] then writeln ("Warning: Theorem " ^ name ^
+  in if consts = [] then warning ("Theorem " ^ name ^
                                   " cannot be stored in ThmDB\n\t because it \
                                   \contains no or only ignored constants.")
      else if is_some const_idx' then
isabelle