# HG changeset patch
# User wenzelm
# Date 963523214 -7200
# Node ID 07598d493d331236e0a1452ca3e2199fb6b29dab
# Parent  1625c1f172b34d6ab646a1c78fcb62445e539076
tuned;

diff -r 1625c1f172b3 -r 07598d493d33 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Thu Jul 13 23:19:40 2000 +0200
+++ b/src/Pure/Thy/thy_info.ML	Thu Jul 13 23:20:14 2000 +0200
@@ -81,9 +81,8 @@
 
 (* 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)
@@ -126,7 +125,7 @@
 (* 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);
@@ -157,7 +156,7 @@
       (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]);
 
 
@@ -417,7 +416,7 @@
 
     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