# HG changeset patch # User haftmann # Date 1283349109 -7200 # Node ID 139aada5caf8d05c2c32ca1bd7d629934f588c19 # Parent ac0f24f850c984ecc8751f093f5840dcdb07157b Graph.map, in analogy to Table.map diff -r ac0f24f850c9 -r 139aada5caf8 src/HOL/Imperative_HOL/Heap_Monad.thy --- a/src/HOL/Imperative_HOL/Heap_Monad.thy Wed Sep 01 15:33:59 2010 +0200 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Wed Sep 01 15:51:49 2010 +0200 @@ -578,7 +578,7 @@ (map o pairself) imp_monad_bind pats), imp_monad_bind t0); - in (Graph.map_nodes o map_terms_stmt) imp_monad_bind end; + in (Graph.map o K o map_terms_stmt) imp_monad_bind end; in diff -r ac0f24f850c9 -r 139aada5caf8 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Sep 01 15:33:59 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Sep 01 15:51:49 2010 +0200 @@ -310,7 +310,7 @@ val predfun_neg_intro_of = #neg_intro ooo the_predfun_data val intros_graph_of = - Graph.map_nodes (#intros o rep_pred_data) o PredData.get o ProofContext.theory_of + Graph.map (K (#intros o rep_pred_data)) o PredData.get o ProofContext.theory_of (* diagnostic display functions *) diff -r ac0f24f850c9 -r 139aada5caf8 src/Pure/General/graph.ML --- a/src/Pure/General/graph.ML Wed Sep 01 15:33:59 2010 +0200 +++ b/src/Pure/General/graph.ML Wed Sep 01 15:51:49 2010 +0200 @@ -21,7 +21,7 @@ val maximals: 'a T -> key list val subgraph: (key -> bool) -> 'a T -> 'a T val get_entry: 'a T -> key -> 'a * (key list * key list) (*exception UNDEF*) - val map_nodes: ('a -> 'b) -> 'a T -> 'b T + val map: (key -> 'a -> 'b) -> 'a T -> 'b T val get_node: 'a T -> key -> 'a (*exception UNDEF*) val map_node: key -> ('a -> 'a) -> 'a T -> 'a T val map_node_yield: key -> ('a -> 'b * 'a) -> 'a T -> 'b * 'a T @@ -114,7 +114,7 @@ (* nodes *) -fun map_nodes f (Graph tab) = Graph (Table.map (K (apfst f)) tab); +fun map_nodes f (Graph tab) = Graph (Table.map (apfst o f) tab); fun get_node G = #1 o get_entry G; @@ -286,6 +286,7 @@ (*final declarations of this structure!*) +val map = map_nodes; val fold = fold_graph; end; diff -r ac0f24f850c9 -r 139aada5caf8 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Wed Sep 01 15:33:59 2010 +0200 +++ b/src/Pure/Thy/thy_info.ML Wed Sep 01 15:51:49 2010 +0200 @@ -346,6 +346,6 @@ (* finish all theories *) -fun finish () = change_thys (Graph.map_nodes (fn (_, entry) => (NONE, entry))); +fun finish () = change_thys (Graph.map (fn _ => fn (_, entry) => (NONE, entry))); end;