src/Pure/Thy/present.ML

 (*retrieve graph data from initial collection of theories*)
 fun init_graph remote_path curr_sess = rev o map (fn thy =>
   let
     val name = Context.theory_name thy;
     val {name = sess_name, session, is_local} = get_info thy;
-    val path' = Path.append (Path.make session) (html_path name);
     val entry =
      {name = name, ID = ID_of session name, dir = sess_name,
       path =
         if null session then "" else
         if is_some remote_path andalso not is_local then

 fun init_theory_info name info =
   change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
     (Symtab.update (name, info) theories, files, tex_index, html_index, graph));
 
 fun change_theory_info name f =
-  change_browser_info (fn (info as (theories, files, tex_index, html_index, graph)) =>
+  change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
     (case Symtab.lookup theories name of
       NONE => error ("Browser info: cannot access theory document " ^ quote name)
     | SOME info => (Symtab.update (name, map_theory_info f info) theories, files,
         tex_index, html_index, graph)));
 

   else change_theory_info name (fn (tex_source, html_source, html) =>
     (Buffer.add txt tex_source, html_source, html));
 
 fun add_html_source name txt = change_theory_info name (fn (tex_source, html_source, html) =>
   (tex_source, Buffer.add txt html_source, html));
-
-fun add_html name txt = change_theory_info name (fn (tex_source, html_source, html) =>
-  (tex_source, html_source, Buffer.add txt html));
 
 
 
 (** global session state **)