1.1 --- a/src/Pure/General/graph.ML	Fri Feb 24 22:46:44 2012 +0100
     1.2 +++ b/src/Pure/General/graph.ML	Sat Feb 25 12:34:56 2012 +0100
     1.3 @@ -43,7 +43,6 @@
     1.4    val is_maximal: 'a T -> key -> bool
     1.5    val new_node: key * 'a -> 'a T -> 'a T                              (*exception DUP*)
     1.6    val default_node: key * 'a -> 'a T -> 'a T
     1.7 -  val del_nodes: key list -> 'a T -> 'a T                             (*exception UNDEF*)
     1.8    val del_node: key -> 'a T -> 'a T                                   (*exception UNDEF*)
     1.9    val is_edge: 'a T -> key * key -> bool
    1.10    val add_edge: key * key -> 'a T -> 'a T                             (*exception UNDEF*)
    1.11 @@ -183,12 +182,6 @@
    1.12  fun default_node (x, info) (Graph tab) =
    1.13    Graph (Table.default (x, (info, (Keys.empty, Keys.empty))) tab);
    1.14  
    1.15 -fun del_nodes xs (Graph tab) =
    1.16 -  Graph (tab
    1.17 -    |> fold Table.delete xs
    1.18 -    |> Table.map (fn _ => fn (i, (preds, succs)) =>
    1.19 -      (i, (fold Keys.remove xs preds, fold Keys.remove xs succs))));
    1.20 -
    1.21  fun del_node x (G as Graph tab) =
    1.22    let
    1.23      fun del_adjacent which y =

     2.1 --- a/src/Pure/Thy/thy_info.ML	Fri Feb 24 22:46:44 2012 +0100
     2.2 +++ b/src/Pure/Thy/thy_info.ML	Sat Feb 25 12:34:56 2012 +0100
     2.3 @@ -146,7 +146,7 @@
     2.4        val succs = thy_graph Graph.all_succs [name];
     2.5        val _ = Output.urgent_message (loader_msg "removing" succs);
     2.6        val _ = List.app (perform Remove) succs;
     2.7 -      val _ = change_thys (Graph.del_nodes succs);
     2.8 +      val _ = change_thys (fold Graph.del_node succs);
     2.9      in () end);
    2.10  
    2.11  fun kill_thy name = NAMED_CRITICAL "Thy_Info" (fn () =>

     3.1 --- a/src/Tools/Code/code_thingol.ML	Fri Feb 24 22:46:44 2012 +0100
     3.2 +++ b/src/Tools/Code/code_thingol.ML	Sat Feb 25 12:34:56 2012 +0100
     3.3 @@ -938,7 +938,7 @@
     3.4          val Fun (_, ((vs_ty, [(([], t), _)]), _)) =
     3.5            Graph.get_node program1 Term.dummy_patternN;
     3.6          val deps = Graph.immediate_succs program1 Term.dummy_patternN;
     3.7 -        val program2 = Graph.del_nodes [Term.dummy_patternN] program1;
     3.8 +        val program2 = Graph.del_node Term.dummy_patternN program1;
     3.9          val deps_all = Graph.all_succs program2 deps;
    3.10          val program3 = Graph.restrict (member (op =) deps_all) program2;
    3.11        in (((naming, program3), ((vs_ty, t), deps)), (dep, (naming, program2))) end;

     4.1 --- a/src/Tools/subtyping.ML	Fri Feb 24 22:46:44 2012 +0100
     4.2 +++ b/src/Tools/subtyping.ML	Sat Feb 25 12:34:56 2012 +0100
     4.3 @@ -522,7 +522,7 @@
     4.4          val T = Type_Infer.deref tye (hd nodes);
     4.5          val P = new_imm_preds G nodes;
     4.6          val S = new_imm_succs G nodes;
     4.7 -        val G' = Typ_Graph.del_nodes (tl nodes) G;
     4.8 +        val G' = fold Typ_Graph.del_node (tl nodes) G;
     4.9          fun check_and_gen super T' =
    4.10            let val U = Type_Infer.deref tye T';
    4.11            in