--- 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
--- 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)
--- 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
--- 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 =
--- 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;
--- 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;
--- 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))
--- 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);
--- 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;
--- 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;