# HG changeset patch
# User wenzelm
# Date 1330169696 -3600
# Node ID 919dfcdf6d8a90e25886c73f89cf267f2dcb2a14
# Parent  1f6c140f9c72e0a0047064255e92e6a19c34a710
discontinued slightly odd Graph.del_nodes (inefficient due to full Table.map);

diff -r 1f6c140f9c72 -r 919dfcdf6d8a src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Fri Feb 24 22:46:44 2012 +0100
+++ b/src/Pure/General/graph.ML	Sat Feb 25 12:34:56 2012 +0100
@@ -43,7 +43,6 @@
   val is_maximal: 'a T -> key -> bool
   val new_node: key * 'a -> 'a T -> 'a T                              (*exception DUP*)
   val default_node: key * 'a -> 'a T -> 'a T
-  val del_nodes: key list -> 'a T -> 'a T                             (*exception UNDEF*)
   val del_node: key -> 'a T -> 'a T                                   (*exception UNDEF*)
   val is_edge: 'a T -> key * key -> bool
   val add_edge: key * key -> 'a T -> 'a T                             (*exception UNDEF*)
@@ -183,12 +182,6 @@
 fun default_node (x, info) (Graph tab) =
   Graph (Table.default (x, (info, (Keys.empty, Keys.empty))) tab);
 
-fun del_nodes xs (Graph tab) =
-  Graph (tab
-    |> fold Table.delete xs
-    |> Table.map (fn _ => fn (i, (preds, succs)) =>
-      (i, (fold Keys.remove xs preds, fold Keys.remove xs succs))));
-
 fun del_node x (G as Graph tab) =
   let
     fun del_adjacent which y =
diff -r 1f6c140f9c72 -r 919dfcdf6d8a src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Fri Feb 24 22:46:44 2012 +0100
+++ b/src/Pure/Thy/thy_info.ML	Sat Feb 25 12:34:56 2012 +0100
@@ -146,7 +146,7 @@
       val succs = thy_graph Graph.all_succs [name];
       val _ = Output.urgent_message (loader_msg "removing" succs);
       val _ = List.app (perform Remove) succs;
-      val _ = change_thys (Graph.del_nodes succs);
+      val _ = change_thys (fold Graph.del_node succs);
     in () end);
 
 fun kill_thy name = NAMED_CRITICAL "Thy_Info" (fn () =>
diff -r 1f6c140f9c72 -r 919dfcdf6d8a src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Fri Feb 24 22:46:44 2012 +0100
+++ b/src/Tools/Code/code_thingol.ML	Sat Feb 25 12:34:56 2012 +0100
@@ -938,7 +938,7 @@
         val Fun (_, ((vs_ty, [(([], t), _)]), _)) =
           Graph.get_node program1 Term.dummy_patternN;
         val deps = Graph.immediate_succs program1 Term.dummy_patternN;
-        val program2 = Graph.del_nodes [Term.dummy_patternN] program1;
+        val program2 = Graph.del_node Term.dummy_patternN program1;
         val deps_all = Graph.all_succs program2 deps;
         val program3 = Graph.restrict (member (op =) deps_all) program2;
       in (((naming, program3), ((vs_ty, t), deps)), (dep, (naming, program2))) end;
diff -r 1f6c140f9c72 -r 919dfcdf6d8a src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Fri Feb 24 22:46:44 2012 +0100
+++ b/src/Tools/subtyping.ML	Sat Feb 25 12:34:56 2012 +0100
@@ -522,7 +522,7 @@
         val T = Type_Infer.deref tye (hd nodes);
         val P = new_imm_preds G nodes;
         val S = new_imm_succs G nodes;
-        val G' = Typ_Graph.del_nodes (tl nodes) G;
+        val G' = fold Typ_Graph.del_node (tl nodes) G;
         fun check_and_gen super T' =
           let val U = Type_Infer.deref tye T';
           in