src/Pure/Thy/thy_read.ML

        let val ThyInfo {path = abs_path, ...} = the tinfo;
            val (thy_file, ml_file) = if abs_path = "" then new_filename ()
                                      else (find_file abs_path (name ^ ".thy"),
                                            find_file abs_path (name ^ ".ML"))
        in if thy_file = "" andalso ml_file = "" then
-            (writeln ("Warning: File \"" ^ (tack_on path name)
+            (warning ("File \"" ^ (tack_on path name)
                       ^ ".thy\"\ncontaining theory \"" ^ name
                       ^ "\" no longer exists.");
              new_filename ()
             )
           else (thy_file, ml_file)

         val relatives =
           filter (fn s => s mem wanted_theories) (parents_of_name tname);
       in mk_entry relatives end;
   in if is_some (!cur_htmlfile) then
        (close_out (the (!cur_htmlfile));
-        writeln "Warning: Last theory's HTML file has not been closed.")
+        warning "Last theory's HTML file has not been closed.")
      else ();
      cur_htmlfile := Some (open_out (tack_on tpath ("." ^ tname ^ ".html")));
      cur_has_title := false;
      output (the (!cur_htmlfile), gettext (tack_on tpath tname ^ ".thy"));
 

                 val tpath = tack_on rel_path ("." ^ tname);
 
                 val fname = tack_on path ("." ^ t ^ "_sub.html");
                 val out = if file_exists fname then
                             open_append fname  handle Io s =>
-                              (writeln ("Warning: Unable to write to file ." ^
+                              (warning ("Unable to write to file ." ^
                                         fname); raise Io s)
                           else raise MK_HTML;
             in output (out,
                  " |\n \\__<A HREF=\"" ^
                  tack_on rel_path ("." ^ tname) ^ ".html\">" ^ tname ^

       thyinfo_of_sign (#sign (rep_thm thm))
 
     val (thms', duplicate) = (Symtab.update_new ((name, thm), thms), false)
       handle Symtab.DUPLICATE s => 
         (if eq_thm (the (Symtab.lookup (thms, name)), thm) then 
-           (writeln ("Warning: Theory database already contains copy of\
+           (warning ("Theory database already contains copy of\
                      \ theorem " ^ quote name);
             (thms, true))
          else error ("Duplicate theorem name " ^ quote s
                      ^ " used in theory database"));
 

      cd (!base_path);
      base_path := pwd();
      cd cwd;
 
      if cwd subdir_of (!base_path) then ()
-     else writeln "Warning: The current working directory seems to be no \
+     else warning "The current working directory seems to be no \
                   \subdirectory of\nIsabelle's main directory. \
                   \Please ensure that base_path's value is correct.\n";
 
      writeln ("Setting path for index.html to " ^ quote cwd ^
               "\nGIF path has been set to " ^ quote (!gif_path));