# HG changeset patch
# User haftmann
# Date 1283348039 -7200
# Node ID ac0f24f850c984ecc8751f093f5840dcdb07157b
# Parent  bfd0c0e4dbeed91c94ee463bd31954398fa8691c
replaced Table.map' by Table.map

diff -r bfd0c0e4dbee -r ac0f24f850c9 src/HOL/Boogie/Tools/boogie_vcs.ML
--- a/src/HOL/Boogie/Tools/boogie_vcs.ML	Wed Sep 01 15:10:12 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_vcs.ML	Wed Sep 01 15:33:59 2010 +0200
@@ -348,6 +348,6 @@
   let
     fun rewr (_, (t, _)) = vc_of_term (f thy t)
       |> (fn vc => (vc, (t, thm_of thy vc)))
-  in VCs.map (Option.map (fn (vcs, _) => (Symtab.map rewr vcs, g))) thy end
+  in VCs.map (Option.map (fn (vcs, _) => (Symtab.map (K rewr) vcs, g))) thy end
 
 end
diff -r bfd0c0e4dbee -r ac0f24f850c9 src/HOL/Tools/SMT/smt_monomorph.ML
--- a/src/HOL/Tools/SMT/smt_monomorph.ML	Wed Sep 01 15:10:12 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_monomorph.ML	Wed Sep 01 15:33:59 2010 +0200
@@ -133,7 +133,7 @@
     fun complete (vT as (v, _)) subst =
       subst
       |> not (Vartab.defined subst v) ? Vartab.update vT
-      |> Vartab.map (apsnd (Term.map_atyps (replace vT)))
+      |> Vartab.map (K (apsnd (Term.map_atyps (replace vT))))
 
     fun cert (ix, (S, T)) = pairself (Thm.ctyp_of thy) (TVar (ix, S), T)
 
diff -r bfd0c0e4dbee -r ac0f24f850c9 src/HOL/Tools/SMT/z3_proof_parser.ML
--- a/src/HOL/Tools/SMT/z3_proof_parser.ML	Wed Sep 01 15:10:12 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_parser.ML	Wed Sep 01 15:33:59 2010 +0200
@@ -191,7 +191,7 @@
     fun cert @{term True} = @{cterm "~False"}
       | cert t = certify ctxt' t
 
-  in (typs, Symtab.map cert terms, Inttab.empty, Inttab.empty, [], ctxt') end
+  in (typs, Symtab.map (K cert) terms, Inttab.empty, Inttab.empty, [], ctxt') end
 
 fun fresh_name n (typs, terms, exprs, steps, vars, ctxt) =
   let val (n', ctxt') = yield_singleton Variable.variant_fixes n ctxt
diff -r bfd0c0e4dbee -r ac0f24f850c9 src/HOL/Tools/SMT/z3_proof_reconstruction.ML
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Wed Sep 01 15:10:12 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Wed Sep 01 15:33:59 2010 +0200
@@ -823,7 +823,7 @@
 
     fun result (p, (cx, _)) = (thm_of p, cx)
   in
-    (fn (idx, ptab) => result (lookup idx (ctxt, Inttab.map Unproved ptab)))
+    (fn (idx, ptab) => result (lookup idx (ctxt, Inttab.map (K Unproved) ptab)))
   end
 
 fun reconstruct (output, {typs, terms, unfolds, assms}) ctxt =
diff -r bfd0c0e4dbee -r ac0f24f850c9 src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Wed Sep 01 15:10:12 2010 +0200
+++ b/src/Pure/General/graph.ML	Wed Sep 01 15:33:59 2010 +0200
@@ -114,7 +114,7 @@
 
 (* nodes *)
 
-fun map_nodes f (Graph tab) = Graph (Table.map (fn (i, ps) => (f i, ps)) tab);
+fun map_nodes f (Graph tab) = Graph (Table.map (K (apfst f)) tab);
 
 fun get_node G = #1 o get_entry G;
 
@@ -161,7 +161,7 @@
 fun del_nodes xs (Graph tab) =
   Graph (tab
     |> fold Table.delete xs
-    |> Table.map (fn (i, (preds, succs)) =>
+    |> Table.map (fn _ => fn (i, (preds, succs)) =>
       (i, (fold remove_key xs preds, fold remove_key xs succs))));
 
 fun del_node x (G as Graph tab) =
@@ -206,13 +206,13 @@
 fun join f (G1 as Graph tab1, G2 as Graph tab2) =
   let fun join_node key ((i1, edges1), (i2, _)) = (f key (i1, i2), edges1) in
     if pointer_eq (G1, G2) then G1
-    else fold add_edge (edges G2) (Graph (Table.join join_node (tab1, Table.map no_edges tab2)))
+    else fold add_edge (edges G2) (Graph (Table.join join_node (tab1, Table.map (K no_edges) tab2)))
   end;
 
 fun gen_merge add eq (G1 as Graph tab1, G2 as Graph tab2) =
   let fun eq_node ((i1, _), (i2, _)) = eq (i1, i2) in
     if pointer_eq (G1, G2) then G1
-    else fold add (edges G2) (Graph (Table.merge eq_node (tab1, Table.map no_edges tab2)))
+    else fold add (edges G2) (Graph (Table.merge eq_node (tab1, Table.map (K no_edges) tab2)))
   end;
 
 fun merge eq GG = gen_merge add_edge eq GG;
diff -r bfd0c0e4dbee -r ac0f24f850c9 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Wed Sep 01 15:10:12 2010 +0200
+++ b/src/Pure/General/table.ML	Wed Sep 01 15:33:59 2010 +0200
@@ -20,8 +20,7 @@
   exception UNDEF of key
   val empty: 'a table
   val is_empty: 'a table -> bool
-  val map: ('a -> 'b) -> 'a table -> 'b table
-  val map': (key -> 'a -> 'b) -> 'a table -> 'b table
+  val map: (key -> 'a -> 'b) -> 'a table -> 'b table
   val fold: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a
   val fold_rev: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a
   val dest: 'a table -> (key * 'a) list
@@ -403,8 +402,7 @@
 
 
 (*final declarations of this structure!*)
-fun map f = map_table (K f);
-val map' = map_table;
+val map = map_table;
 val fold = fold_table;
 val fold_rev = fold_rev_table;
 
diff -r bfd0c0e4dbee -r ac0f24f850c9 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Wed Sep 01 15:10:12 2010 +0200
+++ b/src/Pure/Isar/code.ML	Wed Sep 01 15:33:59 2010 +0200
@@ -282,7 +282,7 @@
   then NONE
   else thy
     |> (Code_Data.map o apfst)
-        ((map_functions o Symtab.map) (fn ((changed, current), history) =>
+        ((map_functions o Symtab.map) (fn _ => fn ((changed, current), history) =>
           ((false, current),
             if changed then (serial (), current) :: history else history))
         #> map_history_concluded (K true))
diff -r bfd0c0e4dbee -r ac0f24f850c9 src/Pure/context.ML
--- a/src/Pure/context.ML	Wed Sep 01 15:10:12 2010 +0200
+++ b/src/Pure/context.ML	Wed Sep 01 15:33:59 2010 +0200
@@ -137,7 +137,7 @@
     val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, kind)));
   in k end;
 
-val extend_data = Datatab.map' invoke_extend;
+val extend_data = Datatab.map invoke_extend;
 
 fun merge_data pp (data1, data2) =
   Datatab.keys (Datatab.merge (K true) (data1, data2))
@@ -476,7 +476,7 @@
   | NONE => raise Fail "Invalid proof data identifier");
 
 fun init_data thy =
-  Datatab.map' (fn k => fn _ => invoke_init k thy) (! kinds);
+  Datatab.map (fn k => fn _ => invoke_init k thy) (! kinds);
 
 fun init_new_data data thy =
   Datatab.merge (K true) (data, init_data thy);
diff -r bfd0c0e4dbee -r ac0f24f850c9 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Wed Sep 01 15:10:12 2010 +0200
+++ b/src/Pure/proofterm.ML	Wed Sep 01 15:33:59 2010 +0200
@@ -515,7 +515,7 @@
   | remove_types t = t;
 
 fun remove_types_env (Envir.Envir {maxidx, tenv, tyenv}) =
-  Envir.Envir {maxidx = maxidx, tenv = Vartab.map (apsnd remove_types) tenv, tyenv = tyenv};
+  Envir.Envir {maxidx = maxidx, tenv = Vartab.map (K (apsnd remove_types)) tenv, tyenv = tyenv};
 
 fun norm_proof' env prf = norm_proof (remove_types_env env) prf;
 
diff -r bfd0c0e4dbee -r ac0f24f850c9 src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Wed Sep 01 15:10:12 2010 +0200
+++ b/src/Pure/sorts.ML	Wed Sep 01 15:33:59 2010 +0200
@@ -321,7 +321,7 @@
         | NONE => NONE)
       else NONE;
     val classes' = classes |> Graph.subgraph P;
-    val arities' = arities |> Symtab.map' (map_filter o restrict_arity);
+    val arities' = arities |> Symtab.map (map_filter o restrict_arity);
   in (restrict_sort, rebuild_arities pp (make_algebra (classes', arities'))) end;