--- a/src/CTT/CTT.ML Tue Sep 20 08:20:22 2005 +0200
+++ b/src/CTT/CTT.ML Tue Sep 20 08:21:49 2005 +0200
@@ -157,7 +157,7 @@
(*0 subgoals vs 1 or more*)
val (safe0_brls, safep_brls) =
- List.partition (apl(0,op=) o subgoals_of_brl) safe_brls;
+ List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls;
fun safestep_tac thms i =
form_tac ORELSE
--- a/src/CTT/rew.ML Tue Sep 20 08:20:22 2005 +0200
+++ b/src/CTT/rew.ML Tue Sep 20 08:21:49 2005 +0200
@@ -9,7 +9,7 @@
(*Make list of ProdE RS ProdE ... RS ProdE RS EqE
for using assumptions as rewrite rules*)
fun peEs 0 = []
- | peEs n = EqE :: map (apl(ProdE, op RS)) (peEs (n-1));
+ | peEs n = EqE :: map (curry (op RS) ProdE) (peEs (n-1));
(*Tactic used for proving conditions for the cond_rls*)
val prove_cond_tac = eresolve_tac (peEs 5);
--- a/src/FOL/intprover.ML Tue Sep 20 08:20:22 2005 +0200
+++ b/src/FOL/intprover.ML Tue Sep 20 08:21:49 2005 +0200
@@ -60,7 +60,7 @@
(*0 subgoals vs 1 or more: the p in safep is for positive*)
val (safe0_brls, safep_brls) =
- List.partition (apl(0,op=) o subgoals_of_brl) safe_brls;
+ List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls;
(*Attack subgoals using safe inferences -- matching, not resolution*)
val safe_step_tac = FIRST' [eq_assume_tac,
--- a/src/FOLP/classical.ML Tue Sep 20 08:20:22 2005 +0200
+++ b/src/FOLP/classical.ML Tue Sep 20 08:21:49 2005 +0200
@@ -112,7 +112,7 @@
(*Note that allE precedes exI in haz_brls*)
fun make_cs {safeIs,safeEs,hazIs,hazEs} =
let val (safe0_brls, safep_brls) = (*0 subgoals vs 1 or more*)
- List.partition (apl(0,op=) o subgoals_of_brl)
+ List.partition (curry (op =) 0 o subgoals_of_brl)
(sort (make_ord lessb) (joinrules(safeIs, safeEs)))
in CS{safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs,
safe0_brls=safe0_brls, safep_brls=safep_brls,
--- a/src/FOLP/intprover.ML Tue Sep 20 08:20:22 2005 +0200
+++ b/src/FOLP/intprover.ML Tue Sep 20 08:21:49 2005 +0200
@@ -50,7 +50,7 @@
(*0 subgoals vs 1 or more: the p in safep is for positive*)
val (safe0_brls, safep_brls) =
- List.partition (apl(0,op=) o subgoals_of_brl) safe_brls;
+ List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls;
(*Attack subgoals using safe inferences*)
val safe_step_tac = FIRST' [uniq_assume_tac,
--- a/src/HOL/Tools/recdef_package.ML Tue Sep 20 08:20:22 2005 +0200
+++ b/src/HOL/Tools/recdef_package.ML Tue Sep 20 08:21:49 2005 +0200
@@ -245,7 +245,7 @@
val (thy, {rules = rules_idx, induct, tcs}) =
tfl_fn strict thy cs (ss delcongs [imp_cong])
congs wfs name R eqs;
- val rules = map (map #1) (Library.partition_eq Library.eq_snd rules_idx);
+ val rules = map (map #1) (Library.partition_eq (Library.eq_snd (op =)) rules_idx);
val simp_att = if null tcs then
[Simplifier.simp_add_global, RecfunCodegen.add NONE] else [];
--- a/src/Provers/Arith/fast_lin_arith.ML Tue Sep 20 08:20:22 2005 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Tue Sep 20 08:21:49 2005 +0200
@@ -278,7 +278,7 @@
if n = 1 then i
else if n = 0 andalso ty = Lt then sys_error "multiply_ineq"
else if n < 0 andalso (ty=Le orelse ty=Lt) then sys_error "multiply_ineq"
- else Lineq(n * k,ty,map (apl(n,op * )) l,Multiplied(n,just));
+ else Lineq (n * k, ty, map (curry (op *) n) l, Multiplied (n, just));
(* ------------------------------------------------------------------------- *)
(* Add together (in)equations. *)
@@ -317,7 +317,7 @@
case ty of Eq => k <> 0 | Le => k > 0 | Lt => k >= 0;
fun calc_blowup (l:IntInf.int list) =
- let val (p,n) = List.partition (apl(0,op<)) (List.filter (apl(0,op<>)) l)
+ let val (p,n) = List.partition (curry (op <) 0) (List.filter (curry (op <>) 0) l)
in (length p) * (length n) end;
(* ------------------------------------------------------------------------- *)
@@ -538,11 +538,11 @@
in a ^ " = " ^ s end;
fun print_ex sds =
- tracing o
- apl("Counter example:\n",op ^) o
- commas o
- map print_atom o
- apl(sds, op ~~);
+ curry (op ~~) sds
+ #> map print_atom
+ #> commas
+ #> curry (op ^) "Counter example:\n"
+ #> tracing;
fun trace_ex(sg,params,atoms,discr,n,hist:history) =
if null hist then ()
--- a/src/Pure/Isar/attrib.ML Tue Sep 20 08:20:22 2005 +0200
+++ b/src/Pure/Isar/attrib.ML Tue Sep 20 08:21:49 2005 +0200
@@ -72,7 +72,7 @@
val copy = I;
val extend = I;
- fun merge _ tables = NameSpace.merge_tables eq_snd tables handle Symtab.DUPS dups =>
+ fun merge _ tables = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUPS dups =>
error ("Attempt to merge different versions of attribute(s) " ^ commas_quote dups);
fun print _ attribs =
--- a/src/Pure/Isar/context_rules.ML Tue Sep 20 08:20:22 2005 +0200
+++ b/src/Pure/Isar/context_rules.ML Tue Sep 20 08:21:49 2005 +0200
@@ -131,7 +131,7 @@
fun merge _ (Rules {rules = rules1, wrappers = (ws1, ws1'), ...},
Rules {rules = rules2, wrappers = (ws2, ws2'), ...}) =
let
- val wrappers = (gen_merge_lists' eq_snd ws1 ws2, gen_merge_lists' eq_snd ws1' ws2');
+ val wrappers = (gen_merge_lists' (eq_snd (op =)) ws1 ws2, gen_merge_lists' (eq_snd (op =)) ws1' ws2');
val rules = gen_merge_lists' (fn ((_, (k1, th1)), (_, (k2, th2))) =>
k1 = k2 andalso Drule.eq_thm_prop (th1, th2)) rules1 rules2;
val next = ~ (length rules);
--- a/src/Pure/Isar/locale.ML Tue Sep 20 08:20:22 2005 +0200
+++ b/src/Pure/Isar/locale.ML Tue Sep 20 08:21:49 2005 +0200
@@ -372,7 +372,7 @@
fun join_locs _ ({predicate, import, elems, params, regs}: locale,
{elems = elems', regs = regs', ...}: locale) =
SOME {predicate = predicate, import = import,
- elems = gen_merge_lists eq_snd elems elems',
+ elems = gen_merge_lists (eq_snd (op =)) elems elems',
params = params,
regs = merge_alists regs regs'};
fun merge _ ((space1, locs1, regs1), (space2, locs2, regs2)) =
@@ -770,10 +770,10 @@
val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (List.mapPartial I Vs));
in map (Option.map (Envir.norm_type unifier')) Vs end;
-fun params_of elemss = gen_distinct eq_fst (List.concat (map (snd o fst) elemss));
-fun params_of' elemss = gen_distinct eq_fst (List.concat (map (snd o fst o fst) elemss));
+fun params_of elemss = gen_distinct (eq_fst (op =)) (List.concat (map (snd o fst) elemss));
+fun params_of' elemss = gen_distinct (eq_fst (op =)) (List.concat (map (snd o fst o fst) elemss));
fun params_syn_of syn elemss =
- gen_distinct eq_fst (List.concat (map (snd o fst) elemss)) |>
+ gen_distinct (eq_fst (op =)) (List.concat (map (snd o fst) elemss)) |>
map (apfst (fn x => (x, valOf (Symtab.lookup syn x))));
@@ -843,7 +843,7 @@
val (unifier, _) = Library.foldl unify_list
((Vartab.empty, maxidx), map #2 (Symtab.dest (Symtab.make_multi parms)));
- val parms' = map (apsnd (Envir.norm_type unifier)) (gen_distinct eq_fst parms);
+ val parms' = map (apsnd (Envir.norm_type unifier)) (gen_distinct (eq_fst (op =)) parms);
val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms'));
fun inst_parms (i, ps) =
@@ -939,7 +939,7 @@
(* propagate parameter types, to keep them consistent *)
val regs' = map (fn ((name, ps), ths) =>
((name, map (rename ren) ps), ths)) regs;
- val new_regs = gen_rems eq_fst (regs', ids);
+ val new_regs = gen_rems (eq_fst (op =)) (regs', ids);
val new_ids = map fst new_regs;
val new_idTs = map (apsnd (map (fn p => (p, (the o AList.lookup (op =) ps) p)))) new_ids;
@@ -993,7 +993,7 @@
val ren = renaming xs parms'
handle ERROR_MESSAGE msg => err_in_locale' ctxt msg ids';
- val ids'' = gen_distinct eq_fst (map (rename_parms top ren) ids');
+ val ids'' = gen_distinct (eq_fst (op =)) (map (rename_parms top ren) ids');
val parms'' = distinct (List.concat (map (#2 o #1) ids''));
val syn'' = syn' |> Symtab.dest |> map (rename_var ren) |>
Symtab.make;
@@ -1037,7 +1037,7 @@
(* compute identifiers and syntax, merge with previous ones *)
val (ids, _, syn) = identify true expr;
- val idents = gen_rems eq_fst (ids, prev_idents);
+ val idents = gen_rems (eq_fst (op =)) (ids, prev_idents);
val syntax = merge_syntax ctxt ids (syn, prev_syntax);
(* add types to params, check for unique params and unify them *)
val raw_elemss = unique_parms ctxt (map (eval syntax) idents);
--- a/src/Pure/Isar/method.ML Tue Sep 20 08:20:22 2005 +0200
+++ b/src/Pure/Isar/method.ML Tue Sep 20 08:21:49 2005 +0200
@@ -541,7 +541,7 @@
val empty = NameSpace.empty_table;
val copy = I;
val extend = I;
- fun merge _ tables = NameSpace.merge_tables eq_snd tables handle Symtab.DUPS dups =>
+ fun merge _ tables = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUPS dups =>
error ("Attempt to merge different versions of method(s) " ^ commas_quote dups);
fun print _ meths =
--- a/src/Pure/Isar/proof_context.ML Tue Sep 20 08:20:22 2005 +0200
+++ b/src/Pure/Isar/proof_context.ML Tue Sep 20 08:21:49 2005 +0200
@@ -958,7 +958,7 @@
fun lthms_containing ctxt spec =
FactIndex.find (fact_index_of ctxt) spec
|> List.filter (valid_thms ctxt)
- |> gen_distinct eq_fst;
+ |> gen_distinct (eq_fst (op =));
(* name space operations *)
--- a/src/Pure/Isar/term_style.ML Tue Sep 20 08:20:22 2005 +0200
+++ b/src/Pure/Isar/term_style.ML Tue Sep 20 08:21:49 2005 +0200
@@ -28,7 +28,7 @@
val empty = Symtab.empty;
val copy = I;
val extend = I;
- fun merge _ tabs = Symtab.merge eq_snd tabs
+ fun merge _ tabs = Symtab.merge (eq_snd (op =)) tabs
handle Symtab.DUPS dups => err_dup_styles dups;
fun print _ tab = Pretty.writeln (Pretty.strs ("antiquote styles:" :: Symtab.keys tab));
end);
--- a/src/Pure/Syntax/syntax.ML Tue Sep 20 08:20:22 2005 +0200
+++ b/src/Pure/Syntax/syntax.ML Tue Sep 20 08:21:49 2005 +0200
@@ -108,7 +108,7 @@
(** tables of token translation functions **)
fun lookup_tokentr tabs modes =
- let val trs = gen_distinct eq_fst
+ let val trs = gen_distinct (eq_fst (op =))
(List.concat (map (these o AList.lookup (op =) tabs) (modes @ [""])))
in fn c => Option.map fst (AList.lookup (op =) trs c) end;
@@ -124,7 +124,7 @@
val trs2 = these (AList.lookup (op =) tabs2 mode);
val trs = gen_distinct eq_tr (trs1 @ trs2);
in
- (case gen_duplicates eq_fst trs of
+ (case gen_duplicates (eq_fst (op =)) trs of
[] => (mode, trs)
| dups => error ("More than one token translation function in mode " ^
quote mode ^ " for " ^ commas_quote (map name dups)))
--- a/src/Pure/Thy/present.ML Tue Sep 20 08:20:22 2005 +0200
+++ b/src/Pure/Thy/present.ML Tue Sep 20 08:21:49 2005 +0200
@@ -274,7 +274,7 @@
| _ => error ("Malformed document version specification: " ^ quote str));
fun read_versions strs =
- rev (gen_distinct eq_fst (rev ((documentN, "") :: map read_version strs)))
+ rev (gen_distinct (eq_fst (op =)) (rev ((documentN, "") :: map read_version strs)))
|> filter_out (equal "-" o #2);
--- a/src/Pure/Thy/thy_parse.ML Tue Sep 20 08:20:22 2005 +0200
+++ b/src/Pure/Thy/thy_parse.ML Tue Sep 20 08:21:49 2005 +0200
@@ -284,8 +284,8 @@
[(parens (commas [t, mk_list xs, rhs, syn]), true)];
fun mk_type_decls tys =
- "|> Theory.add_types\n" ^ mk_big_list (keyfilter tys false) ^ "\n\n\
- \|> Theory.add_tyabbrs\n" ^ mk_big_list (keyfilter tys true);
+ "|> Theory.add_types\n" ^ mk_big_list (AList.find (op =) tys false) ^ "\n\n\
+ \|> Theory.add_tyabbrs\n" ^ mk_big_list (AList.find (op =) tys true);
val old_type_decl = names1 -- nat -- opt_infix >> mk_old_type_decl;
@@ -390,8 +390,8 @@
(* instance *)
fun mk_witness (axths, opt_tac) =
- mk_list (keyfilter axths false) ^ "\n" ^
- mk_list (keyfilter axths true) ^ "\n" ^
+ mk_list (AList.find (op =) axths false) ^ "\n" ^
+ mk_list (AList.find (op =) axths true) ^ "\n" ^
opt_tac;
val axm_or_thm =
@@ -441,7 +441,7 @@
fun make_syntax keywords sects =
let
val dups = duplicates (map fst sects);
- val sects' = gen_distinct eq_fst sects;
+ val sects' = gen_distinct (eq_fst (op =)) sects;
val keys = map Symbol.explode (map fst sects' @ keywords);
in
if null dups then ()
--- a/src/Pure/axclass.ML Tue Sep 20 08:20:22 2005 +0200
+++ b/src/Pure/axclass.ML Tue Sep 20 08:21:49 2005 +0200
@@ -103,7 +103,7 @@
Type (t, tys) => (t, map dest_varT tys handle TYPE _ => err ())
| _ => err ());
val ss =
- if null (gen_duplicates eq_fst tvars)
+ if null (gen_duplicates (eq_fst (op =)) tvars)
then map snd tvars else err ();
in (t, ss, c) end;
--- a/src/Pure/meta_simplifier.ML Tue Sep 20 08:20:22 2005 +0200
+++ b/src/Pure/meta_simplifier.ML Tue Sep 20 08:21:49 2005 +0200
@@ -292,7 +292,7 @@
val cngs = map (fn (name, {thm, ...}) => (name, thm)) (#1 congs);
val prcs = Net.entries procs |>
map (fn Proc {name, lhs, id, ...} => ((name, lhs), id))
- |> partition_eq eq_snd
+ |> partition_eq (eq_snd (op =))
|> map (fn ps => (#1 (#1 (hd ps)), map (#2 o #1) ps))
|> Library.sort_wrt #1;
in
--- a/src/Pure/pure_thy.ML Tue Sep 20 08:20:22 2005 +0200
+++ b/src/Pure/pure_thy.ML Tue Sep 20 08:21:49 2005 +0200
@@ -250,7 +250,7 @@
|> map (fn thy =>
FactIndex.find (fact_index_of thy) spec
|> List.filter (fn (name, ths) => valid_thms theory (Name name, ths))
- |> gen_distinct eq_fst)
+ |> gen_distinct (eq_fst (op =)))
|> List.concat;
fun thms_containing_consts thy consts =
--- a/src/Pure/sign.ML Tue Sep 20 08:20:22 2005 +0200
+++ b/src/Pure/sign.ML Tue Sep 20 08:21:49 2005 +0200
@@ -227,7 +227,7 @@
val naming = NameSpace.default_naming;
val syn = Syntax.merge_syntaxes syn1 syn2;
val tsig = Type.merge_tsigs pp (tsig1, tsig2);
- val consts = NameSpace.merge_tables eq_snd (consts1, consts2)
+ val consts = NameSpace.merge_tables (eq_snd (op =)) (consts1, consts2)
handle Symtab.DUPS cs => err_dup_consts cs;
val constraints = Symtab.merge (op =) (constraints1, constraints2)
handle Symtab.DUPS cs => err_inconsistent_constraints cs;
--- a/src/Pure/tactic.ML Tue Sep 20 08:20:22 2005 +0200
+++ b/src/Pure/tactic.ML Tue Sep 20 08:21:49 2005 +0200
@@ -573,9 +573,9 @@
(*folding should handle critical pairs! E.g. K == Inl(0), S == Inr(Inl(0))
Returns longest lhs first to avoid folding its subexpressions.*)
fun sort_lhs_depths defs =
- let val keylist = make_keylist (term_depth o lhs_of_thm) defs
+ let val keylist = AList.make (term_depth o lhs_of_thm) defs
val keys = distinct (sort (rev_order o int_ord) (map #2 keylist))
- in map (keyfilter keylist) keys end;
+ in map (AList.find (op =) keylist) keys end;
val rev_defs = sort_lhs_depths o map symmetric;
--- a/src/Pure/theory.ML Tue Sep 20 08:20:22 2005 +0200
+++ b/src/Pure/theory.ML Tue Sep 20 08:21:49 2005 +0200
@@ -120,7 +120,7 @@
val axioms = NameSpace.empty_table;
val defs = Defs.merge pp defs1 defs2;
- val oracles = NameSpace.merge_tables eq_snd (oracles1, oracles2)
+ val oracles = NameSpace.merge_tables (eq_snd (op =)) (oracles1, oracles2)
handle Symtab.DUPS dups => err_dup_oras dups;
in make_thy (axioms, defs, oracles) end;
--- a/src/Pure/type.ML Tue Sep 20 08:20:22 2005 +0200
+++ b/src/Pure/type.ML Tue Sep 20 08:21:49 2005 +0200
@@ -632,7 +632,7 @@
fun add_nonterminals naming = change_types o fold (new_decl naming) o map (rpair Nonterminal);
fun merge_types (types1, types2) =
- NameSpace.merge_tables Library.eq_snd (types1, types2) handle Symtab.DUPS (d :: _) =>
+ NameSpace.merge_tables (Library.eq_snd (op =)) (types1, types2) handle Symtab.DUPS (d :: _) =>
err_in_decls d (the_decl types1 d) (the_decl types2 d);
end;
--- a/src/Pure/type_infer.ML Tue Sep 20 08:20:22 2005 +0200
+++ b/src/Pure/type_infer.ML Tue Sep 20 08:21:49 2005 +0200
@@ -452,7 +452,7 @@
xi = xi' andalso Type.eq_sort tsig (S, S');
val env = gen_distinct eq (map (apsnd map_sort) raw_env);
- val _ = (case gen_duplicates eq_fst env of [] => ()
+ val _ = (case gen_duplicates (eq_fst (op =)) env of [] => ()
| dups => error ("Inconsistent sort constraints for type variable(s) "
^ commas_quote (map (Syntax.string_of_vname' o fst) dups)));