removed debugging message;
link to non-existing super index is now omitted silently

--- a/src/Pure/Thy/thy_read.ML	Fri Dec 01 12:22:07 1995 +0100
+++ b/src/Pure/Thy/thy_read.ML	Fri Dec 01 12:24:06 1995 +0100
@@ -1104,8 +1104,7 @@
       val subdirs = space_explode "/" subdir;
 
       (*Look for index.html in superdirectories*)
-      fun find_super_index [] _ =
-            error "finish_html: Unable to find super index file."
+      fun find_super_index [] n = ("", n)
         | find_super_index (p::ps) n =
           let val index_path = "/" ^ space_implode "/" (rev ps);
           in if file_exists (index_path ^ "/index.html") then (index_path, n)
@@ -1138,11 +1137,12 @@
        \<IMG SRC = \"" ^ tack_on gif_path "red_arrow.gif\
        \\" ALT = \\/></A> stands for subtheories (child theories)<BR>\n\
        \<IMG SRC = \"" ^ tack_on gif_path "blue_arrow.gif\
-       \\" ALT = /\\></A> stands for supertheories (parent theories)\
-       \<P>\n<A HREF = \"" ^ relative_path (!index_path) super_index ^ 
-       "/index.html\">Back</A> to the index of " ^
-       (if level = 0 then "Isabelle logics"
-        else space_implode "/" (take (level, subdirs))) ^
+       \\" ALT = /\\></A> stands for supertheories (parent theories)" ^
+       (if super_index = "" then "" else
+        ("<P>\n<A HREF = \"" ^ relative_path (!index_path) super_index ^ 
+         "/index.html\">Back</A> to the index of " ^
+         (if level = 0 then "Isabelle logics"
+          else space_implode "/" (take (level, subdirs))))) ^
        "\n" ^
        (if file_exists (tack_on (!index_path) "README.html") then
           "<BR>View the <A HREF = \"README.html\">ReadMe</A> file.\n"
@@ -1151,7 +1151,7 @@
         else "") ^
        "<HR>" ^ implode (map main_entry theories) ^ "<!-->");
      close_out out;
-     if level = 0 then () else link_directory ()
+     if super_index = "" orelse level = 0 then () else link_directory ()
   end;
 
 
@@ -1180,9 +1180,7 @@
                    thy_ss = thy_ss, simpset = simpset,
                    datatypes = (name, cons) :: datatypes}
       | None => error "store_datatype: theory not found";
-  in
-writeln ("*** Storing datatype " ^ name ^ " (" ^ commas cons ^ ") for theory " ^ (!cur_thyname));
-     loaded_thys := Symtab.update ((!cur_thyname, tinfo), !loaded_thys) end;
+  in loaded_thys := Symtab.update ((!cur_thyname, tinfo), !loaded_thys) end;
 
 fun datatypes_of thy =
   let val (_, ThyInfo {datatypes, ...}) = thyinfo_of_sign (sign_of thy);