# HG changeset patch
# User wenzelm
# Date 1420032484 -3600
# Node ID 8521841f277b950a7f263f8b890cca299bfd3f2b
# Parent  2486d625878b98b734eb95405ce9752a551d5e37
tuned;

diff -r 2486d625878b -r 8521841f277b src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Wed Dec 31 14:15:52 2014 +0100
+++ b/src/Pure/Thy/present.ML	Wed Dec 31 14:28:04 2014 +0100
@@ -60,8 +60,8 @@
 
 (** graphs **)
 
-fun ID_of sess s = space_implode "/" (sess @ [s]);
-fun ID_of_thy thy = ID_of (session_chapter_name thy) (Context.theory_name thy);
+fun ident_of sess s = space_implode "/" (sess @ [s]);
+fun ident_of_thy thy = ident_of (session_chapter_name thy) (Context.theory_name thy);
 
 fun theory_link (curr_chapter, curr_session) thy =
   let
@@ -89,11 +89,11 @@
       | SOME p => Path.implode p);
     val graph_entry =
      {name = thy_name,
-      ident = ID_of [chapter, session_name] thy_name,
+      ident = ident_of [chapter, session_name] thy_name,
       directory = session_name,
       path = path,
       unfold = false,
-      parents = map ID_of_thy (Theory.parents_of thy)};
+      parents = map ident_of_thy (Theory.parents_of thy)};
   in (0, graph_entry) end);
 
 fun ins_graph_entry (i, entry as {ident, ...}) (graph: (int * browser_node) list) =
@@ -393,11 +393,11 @@
 
       val graph_entry =
        {name = name,
-        ident = ID_of [chapter, session_name] name,
+        ident = ident_of [chapter, session_name] name,
         directory = session_name,
         unfold = true,
         path = Path.implode (html_path name),
-        parents = map ID_of_thy parents};
+        parents = map ident_of_thy parents};
     in
       init_theory_info name (make_theory_info ("", html_source));
       add_graph_entry (update_time, graph_entry);