src/Pure/Thy/thy_info.ML

 fun cycle_msg name names = loader_msg ("cyclic dependency of " ^ show_path (name :: names)) [];
 
 
 (* derived graph operations *)
 
-fun add_deps name parents G =
-  foldl (fn (H, parent) => Graph.add_edge_acyclic (parent, name) H) (G, parents)
-    handle Graph.CYCLES namess => error (cat_lines (map (cycle_msg name) namess));
+fun add_deps name parents G = Graph.add_deps_acyclic (name, parents) G
+  handle Graph.CYCLES namess => error (cat_lines (map (cycle_msg name) namess));
 
 fun upd_deps name entry G =
   foldl (fn (H, parent) => Graph.del_edge (parent, name) H) (G, Graph.imm_preds G name)
   |> Graph.map_node name (K entry);
 

 
 
 (* access thy *)
 
 fun lookup_thy name =
-  Some (thy_graph Graph.get_node name) handle Graph.UNDEFINED _ => None;
+  Some (thy_graph Graph.get_node name) handle Graph.UNDEF _ => None;
 
 val known_thy = is_some o lookup_thy;
 fun check_known_thy name = known_thy name orelse (warning ("Unknown theory " ^ quote name); false);
 fun if_known_thy f name = if check_known_thy name then f name else ();
 

   | Some {master, files, ...} =>
       (case master of Some m => [#1 (ThyLoad.get_thy m)] | None => []) @
       (mapfilter (apsome #1 o #2) files));
 
 fun get_preds name =
-  (thy_graph Graph.imm_preds name) handle Graph.UNDEFINED _ =>
+  (thy_graph Graph.imm_preds name) handle Graph.UNDEF _ =>
     error (loader_msg "nothing known about theory" [name]);
 
 
 (* access theory *)
 

       else Some y_name;
     val variants = mapfilter get_variant (parents ~~ parent_names);
 
     fun register G =
       (Graph.new_node (name, (None, Some theory)) G
-        handle Graph.DUPLICATE _ => err "duplicate theory entry" [])
+        handle Graph.DUP _ => err "duplicate theory entry" [])
       |> add_deps name parent_names;
   in
     if not (null nonfinished) then err "non-finished parent theories" nonfinished
     else if not (null variants) then err "different versions of parent theories" variants
     else (change_thys register; perform Update name)