1.1 --- a/src/CTT/CTT.ML Tue Sep 20 08:20:22 2005 +0200
1.2 +++ b/src/CTT/CTT.ML Tue Sep 20 08:21:49 2005 +0200
1.3 @@ -157,7 +157,7 @@
1.4
1.5 (*0 subgoals vs 1 or more*)
1.6 val (safe0_brls, safep_brls) =
1.7 - List.partition (apl(0,op=) o subgoals_of_brl) safe_brls;
1.8 + List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls;
1.9
1.10 fun safestep_tac thms i =
1.11 form_tac ORELSE
2.1 --- a/src/CTT/rew.ML Tue Sep 20 08:20:22 2005 +0200
2.2 +++ b/src/CTT/rew.ML Tue Sep 20 08:21:49 2005 +0200
2.3 @@ -9,7 +9,7 @@
2.4 (*Make list of ProdE RS ProdE ... RS ProdE RS EqE
2.5 for using assumptions as rewrite rules*)
2.6 fun peEs 0 = []
2.7 - | peEs n = EqE :: map (apl(ProdE, op RS)) (peEs (n-1));
2.8 + | peEs n = EqE :: map (curry (op RS) ProdE) (peEs (n-1));
2.9
2.10 (*Tactic used for proving conditions for the cond_rls*)
2.11 val prove_cond_tac = eresolve_tac (peEs 5);
3.1 --- a/src/FOL/intprover.ML Tue Sep 20 08:20:22 2005 +0200
3.2 +++ b/src/FOL/intprover.ML Tue Sep 20 08:21:49 2005 +0200
3.3 @@ -60,7 +60,7 @@
3.4
3.5 (*0 subgoals vs 1 or more: the p in safep is for positive*)
3.6 val (safe0_brls, safep_brls) =
3.7 - List.partition (apl(0,op=) o subgoals_of_brl) safe_brls;
3.8 + List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls;
3.9
3.10 (*Attack subgoals using safe inferences -- matching, not resolution*)
3.11 val safe_step_tac = FIRST' [eq_assume_tac,
4.1 --- a/src/FOLP/classical.ML Tue Sep 20 08:20:22 2005 +0200
4.2 +++ b/src/FOLP/classical.ML Tue Sep 20 08:21:49 2005 +0200
4.3 @@ -112,7 +112,7 @@
4.4 (*Note that allE precedes exI in haz_brls*)
4.5 fun make_cs {safeIs,safeEs,hazIs,hazEs} =
4.6 let val (safe0_brls, safep_brls) = (*0 subgoals vs 1 or more*)
4.7 - List.partition (apl(0,op=) o subgoals_of_brl)
4.8 + List.partition (curry (op =) 0 o subgoals_of_brl)
4.9 (sort (make_ord lessb) (joinrules(safeIs, safeEs)))
4.10 in CS{safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs,
4.11 safe0_brls=safe0_brls, safep_brls=safep_brls,
5.1 --- a/src/FOLP/intprover.ML Tue Sep 20 08:20:22 2005 +0200
5.2 +++ b/src/FOLP/intprover.ML Tue Sep 20 08:21:49 2005 +0200
5.3 @@ -50,7 +50,7 @@
5.4
5.5 (*0 subgoals vs 1 or more: the p in safep is for positive*)
5.6 val (safe0_brls, safep_brls) =
5.7 - List.partition (apl(0,op=) o subgoals_of_brl) safe_brls;
5.8 + List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls;
5.9
5.10 (*Attack subgoals using safe inferences*)
5.11 val safe_step_tac = FIRST' [uniq_assume_tac,
6.1 --- a/src/HOL/Tools/recdef_package.ML Tue Sep 20 08:20:22 2005 +0200
6.2 +++ b/src/HOL/Tools/recdef_package.ML Tue Sep 20 08:21:49 2005 +0200
6.3 @@ -245,7 +245,7 @@
6.4 val (thy, {rules = rules_idx, induct, tcs}) =
6.5 tfl_fn strict thy cs (ss delcongs [imp_cong])
6.6 congs wfs name R eqs;
6.7 - val rules = map (map #1) (Library.partition_eq Library.eq_snd rules_idx);
6.8 + val rules = map (map #1) (Library.partition_eq (Library.eq_snd (op =)) rules_idx);
6.9 val simp_att = if null tcs then
6.10 [Simplifier.simp_add_global, RecfunCodegen.add NONE] else [];
6.11
7.1 --- a/src/Provers/Arith/fast_lin_arith.ML Tue Sep 20 08:20:22 2005 +0200
7.2 +++ b/src/Provers/Arith/fast_lin_arith.ML Tue Sep 20 08:21:49 2005 +0200
7.3 @@ -278,7 +278,7 @@
7.4 if n = 1 then i
7.5 else if n = 0 andalso ty = Lt then sys_error "multiply_ineq"
7.6 else if n < 0 andalso (ty=Le orelse ty=Lt) then sys_error "multiply_ineq"
7.7 - else Lineq(n * k,ty,map (apl(n,op * )) l,Multiplied(n,just));
7.8 + else Lineq (n * k, ty, map (curry (op *) n) l, Multiplied (n, just));
7.9
7.10 (* ------------------------------------------------------------------------- *)
7.11 (* Add together (in)equations. *)
7.12 @@ -317,7 +317,7 @@
7.13 case ty of Eq => k <> 0 | Le => k > 0 | Lt => k >= 0;
7.14
7.15 fun calc_blowup (l:IntInf.int list) =
7.16 - let val (p,n) = List.partition (apl(0,op<)) (List.filter (apl(0,op<>)) l)
7.17 + let val (p,n) = List.partition (curry (op <) 0) (List.filter (curry (op <>) 0) l)
7.18 in (length p) * (length n) end;
7.19
7.20 (* ------------------------------------------------------------------------- *)
7.21 @@ -538,11 +538,11 @@
7.22 in a ^ " = " ^ s end;
7.23
7.24 fun print_ex sds =
7.25 - tracing o
7.26 - apl("Counter example:\n",op ^) o
7.27 - commas o
7.28 - map print_atom o
7.29 - apl(sds, op ~~);
7.30 + curry (op ~~) sds
7.31 + #> map print_atom
7.32 + #> commas
7.33 + #> curry (op ^) "Counter example:\n"
7.34 + #> tracing;
7.35
7.36 fun trace_ex(sg,params,atoms,discr,n,hist:history) =
7.37 if null hist then ()
8.1 --- a/src/Pure/Isar/attrib.ML Tue Sep 20 08:20:22 2005 +0200
8.2 +++ b/src/Pure/Isar/attrib.ML Tue Sep 20 08:21:49 2005 +0200
8.3 @@ -72,7 +72,7 @@
8.4 val copy = I;
8.5 val extend = I;
8.6
8.7 - fun merge _ tables = NameSpace.merge_tables eq_snd tables handle Symtab.DUPS dups =>
8.8 + fun merge _ tables = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUPS dups =>
8.9 error ("Attempt to merge different versions of attribute(s) " ^ commas_quote dups);
8.10
8.11 fun print _ attribs =
9.1 --- a/src/Pure/Isar/context_rules.ML Tue Sep 20 08:20:22 2005 +0200
9.2 +++ b/src/Pure/Isar/context_rules.ML Tue Sep 20 08:21:49 2005 +0200
9.3 @@ -131,7 +131,7 @@
9.4 fun merge _ (Rules {rules = rules1, wrappers = (ws1, ws1'), ...},
9.5 Rules {rules = rules2, wrappers = (ws2, ws2'), ...}) =
9.6 let
9.7 - val wrappers = (gen_merge_lists' eq_snd ws1 ws2, gen_merge_lists' eq_snd ws1' ws2');
9.8 + val wrappers = (gen_merge_lists' (eq_snd (op =)) ws1 ws2, gen_merge_lists' (eq_snd (op =)) ws1' ws2');
9.9 val rules = gen_merge_lists' (fn ((_, (k1, th1)), (_, (k2, th2))) =>
9.10 k1 = k2 andalso Drule.eq_thm_prop (th1, th2)) rules1 rules2;
9.11 val next = ~ (length rules);
10.1 --- a/src/Pure/Isar/locale.ML Tue Sep 20 08:20:22 2005 +0200
10.2 +++ b/src/Pure/Isar/locale.ML Tue Sep 20 08:21:49 2005 +0200
10.3 @@ -372,7 +372,7 @@
10.4 fun join_locs _ ({predicate, import, elems, params, regs}: locale,
10.5 {elems = elems', regs = regs', ...}: locale) =
10.6 SOME {predicate = predicate, import = import,
10.7 - elems = gen_merge_lists eq_snd elems elems',
10.8 + elems = gen_merge_lists (eq_snd (op =)) elems elems',
10.9 params = params,
10.10 regs = merge_alists regs regs'};
10.11 fun merge _ ((space1, locs1, regs1), (space2, locs2, regs2)) =
10.12 @@ -770,10 +770,10 @@
10.13 val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (List.mapPartial I Vs));
10.14 in map (Option.map (Envir.norm_type unifier')) Vs end;
10.15
10.16 -fun params_of elemss = gen_distinct eq_fst (List.concat (map (snd o fst) elemss));
10.17 -fun params_of' elemss = gen_distinct eq_fst (List.concat (map (snd o fst o fst) elemss));
10.18 +fun params_of elemss = gen_distinct (eq_fst (op =)) (List.concat (map (snd o fst) elemss));
10.19 +fun params_of' elemss = gen_distinct (eq_fst (op =)) (List.concat (map (snd o fst o fst) elemss));
10.20 fun params_syn_of syn elemss =
10.21 - gen_distinct eq_fst (List.concat (map (snd o fst) elemss)) |>
10.22 + gen_distinct (eq_fst (op =)) (List.concat (map (snd o fst) elemss)) |>
10.23 map (apfst (fn x => (x, valOf (Symtab.lookup syn x))));
10.24
10.25
10.26 @@ -843,7 +843,7 @@
10.27 val (unifier, _) = Library.foldl unify_list
10.28 ((Vartab.empty, maxidx), map #2 (Symtab.dest (Symtab.make_multi parms)));
10.29
10.30 - val parms' = map (apsnd (Envir.norm_type unifier)) (gen_distinct eq_fst parms);
10.31 + val parms' = map (apsnd (Envir.norm_type unifier)) (gen_distinct (eq_fst (op =)) parms);
10.32 val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms'));
10.33
10.34 fun inst_parms (i, ps) =
10.35 @@ -939,7 +939,7 @@
10.36 (* propagate parameter types, to keep them consistent *)
10.37 val regs' = map (fn ((name, ps), ths) =>
10.38 ((name, map (rename ren) ps), ths)) regs;
10.39 - val new_regs = gen_rems eq_fst (regs', ids);
10.40 + val new_regs = gen_rems (eq_fst (op =)) (regs', ids);
10.41 val new_ids = map fst new_regs;
10.42 val new_idTs = map (apsnd (map (fn p => (p, (the o AList.lookup (op =) ps) p)))) new_ids;
10.43
10.44 @@ -993,7 +993,7 @@
10.45 val ren = renaming xs parms'
10.46 handle ERROR_MESSAGE msg => err_in_locale' ctxt msg ids';
10.47
10.48 - val ids'' = gen_distinct eq_fst (map (rename_parms top ren) ids');
10.49 + val ids'' = gen_distinct (eq_fst (op =)) (map (rename_parms top ren) ids');
10.50 val parms'' = distinct (List.concat (map (#2 o #1) ids''));
10.51 val syn'' = syn' |> Symtab.dest |> map (rename_var ren) |>
10.52 Symtab.make;
10.53 @@ -1037,7 +1037,7 @@
10.54
10.55 (* compute identifiers and syntax, merge with previous ones *)
10.56 val (ids, _, syn) = identify true expr;
10.57 - val idents = gen_rems eq_fst (ids, prev_idents);
10.58 + val idents = gen_rems (eq_fst (op =)) (ids, prev_idents);
10.59 val syntax = merge_syntax ctxt ids (syn, prev_syntax);
10.60 (* add types to params, check for unique params and unify them *)
10.61 val raw_elemss = unique_parms ctxt (map (eval syntax) idents);
11.1 --- a/src/Pure/Isar/method.ML Tue Sep 20 08:20:22 2005 +0200
11.2 +++ b/src/Pure/Isar/method.ML Tue Sep 20 08:21:49 2005 +0200
11.3 @@ -541,7 +541,7 @@
11.4 val empty = NameSpace.empty_table;
11.5 val copy = I;
11.6 val extend = I;
11.7 - fun merge _ tables = NameSpace.merge_tables eq_snd tables handle Symtab.DUPS dups =>
11.8 + fun merge _ tables = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUPS dups =>
11.9 error ("Attempt to merge different versions of method(s) " ^ commas_quote dups);
11.10
11.11 fun print _ meths =
12.1 --- a/src/Pure/Isar/proof_context.ML Tue Sep 20 08:20:22 2005 +0200
12.2 +++ b/src/Pure/Isar/proof_context.ML Tue Sep 20 08:21:49 2005 +0200
12.3 @@ -958,7 +958,7 @@
12.4 fun lthms_containing ctxt spec =
12.5 FactIndex.find (fact_index_of ctxt) spec
12.6 |> List.filter (valid_thms ctxt)
12.7 - |> gen_distinct eq_fst;
12.8 + |> gen_distinct (eq_fst (op =));
12.9
12.10
12.11 (* name space operations *)
13.1 --- a/src/Pure/Isar/term_style.ML Tue Sep 20 08:20:22 2005 +0200
13.2 +++ b/src/Pure/Isar/term_style.ML Tue Sep 20 08:21:49 2005 +0200
13.3 @@ -28,7 +28,7 @@
13.4 val empty = Symtab.empty;
13.5 val copy = I;
13.6 val extend = I;
13.7 - fun merge _ tabs = Symtab.merge eq_snd tabs
13.8 + fun merge _ tabs = Symtab.merge (eq_snd (op =)) tabs
13.9 handle Symtab.DUPS dups => err_dup_styles dups;
13.10 fun print _ tab = Pretty.writeln (Pretty.strs ("antiquote styles:" :: Symtab.keys tab));
13.11 end);
14.1 --- a/src/Pure/Syntax/syntax.ML Tue Sep 20 08:20:22 2005 +0200
14.2 +++ b/src/Pure/Syntax/syntax.ML Tue Sep 20 08:21:49 2005 +0200
14.3 @@ -108,7 +108,7 @@
14.4 (** tables of token translation functions **)
14.5
14.6 fun lookup_tokentr tabs modes =
14.7 - let val trs = gen_distinct eq_fst
14.8 + let val trs = gen_distinct (eq_fst (op =))
14.9 (List.concat (map (these o AList.lookup (op =) tabs) (modes @ [""])))
14.10 in fn c => Option.map fst (AList.lookup (op =) trs c) end;
14.11
14.12 @@ -124,7 +124,7 @@
14.13 val trs2 = these (AList.lookup (op =) tabs2 mode);
14.14 val trs = gen_distinct eq_tr (trs1 @ trs2);
14.15 in
14.16 - (case gen_duplicates eq_fst trs of
14.17 + (case gen_duplicates (eq_fst (op =)) trs of
14.18 [] => (mode, trs)
14.19 | dups => error ("More than one token translation function in mode " ^
14.20 quote mode ^ " for " ^ commas_quote (map name dups)))
15.1 --- a/src/Pure/Thy/present.ML Tue Sep 20 08:20:22 2005 +0200
15.2 +++ b/src/Pure/Thy/present.ML Tue Sep 20 08:21:49 2005 +0200
15.3 @@ -274,7 +274,7 @@
15.4 | _ => error ("Malformed document version specification: " ^ quote str));
15.5
15.6 fun read_versions strs =
15.7 - rev (gen_distinct eq_fst (rev ((documentN, "") :: map read_version strs)))
15.8 + rev (gen_distinct (eq_fst (op =)) (rev ((documentN, "") :: map read_version strs)))
15.9 |> filter_out (equal "-" o #2);
15.10
15.11
16.1 --- a/src/Pure/Thy/thy_parse.ML Tue Sep 20 08:20:22 2005 +0200
16.2 +++ b/src/Pure/Thy/thy_parse.ML Tue Sep 20 08:21:49 2005 +0200
16.3 @@ -284,8 +284,8 @@
16.4 [(parens (commas [t, mk_list xs, rhs, syn]), true)];
16.5
16.6 fun mk_type_decls tys =
16.7 - "|> Theory.add_types\n" ^ mk_big_list (keyfilter tys false) ^ "\n\n\
16.8 - \|> Theory.add_tyabbrs\n" ^ mk_big_list (keyfilter tys true);
16.9 + "|> Theory.add_types\n" ^ mk_big_list (AList.find (op =) tys false) ^ "\n\n\
16.10 + \|> Theory.add_tyabbrs\n" ^ mk_big_list (AList.find (op =) tys true);
16.11
16.12
16.13 val old_type_decl = names1 -- nat -- opt_infix >> mk_old_type_decl;
16.14 @@ -390,8 +390,8 @@
16.15 (* instance *)
16.16
16.17 fun mk_witness (axths, opt_tac) =
16.18 - mk_list (keyfilter axths false) ^ "\n" ^
16.19 - mk_list (keyfilter axths true) ^ "\n" ^
16.20 + mk_list (AList.find (op =) axths false) ^ "\n" ^
16.21 + mk_list (AList.find (op =) axths true) ^ "\n" ^
16.22 opt_tac;
16.23
16.24 val axm_or_thm =
16.25 @@ -441,7 +441,7 @@
16.26 fun make_syntax keywords sects =
16.27 let
16.28 val dups = duplicates (map fst sects);
16.29 - val sects' = gen_distinct eq_fst sects;
16.30 + val sects' = gen_distinct (eq_fst (op =)) sects;
16.31 val keys = map Symbol.explode (map fst sects' @ keywords);
16.32 in
16.33 if null dups then ()
17.1 --- a/src/Pure/axclass.ML Tue Sep 20 08:20:22 2005 +0200
17.2 +++ b/src/Pure/axclass.ML Tue Sep 20 08:21:49 2005 +0200
17.3 @@ -103,7 +103,7 @@
17.4 Type (t, tys) => (t, map dest_varT tys handle TYPE _ => err ())
17.5 | _ => err ());
17.6 val ss =
17.7 - if null (gen_duplicates eq_fst tvars)
17.8 + if null (gen_duplicates (eq_fst (op =)) tvars)
17.9 then map snd tvars else err ();
17.10 in (t, ss, c) end;
17.11
18.1 --- a/src/Pure/meta_simplifier.ML Tue Sep 20 08:20:22 2005 +0200
18.2 +++ b/src/Pure/meta_simplifier.ML Tue Sep 20 08:21:49 2005 +0200
18.3 @@ -292,7 +292,7 @@
18.4 val cngs = map (fn (name, {thm, ...}) => (name, thm)) (#1 congs);
18.5 val prcs = Net.entries procs |>
18.6 map (fn Proc {name, lhs, id, ...} => ((name, lhs), id))
18.7 - |> partition_eq eq_snd
18.8 + |> partition_eq (eq_snd (op =))
18.9 |> map (fn ps => (#1 (#1 (hd ps)), map (#2 o #1) ps))
18.10 |> Library.sort_wrt #1;
18.11 in
19.1 --- a/src/Pure/pure_thy.ML Tue Sep 20 08:20:22 2005 +0200
19.2 +++ b/src/Pure/pure_thy.ML Tue Sep 20 08:21:49 2005 +0200
19.3 @@ -250,7 +250,7 @@
19.4 |> map (fn thy =>
19.5 FactIndex.find (fact_index_of thy) spec
19.6 |> List.filter (fn (name, ths) => valid_thms theory (Name name, ths))
19.7 - |> gen_distinct eq_fst)
19.8 + |> gen_distinct (eq_fst (op =)))
19.9 |> List.concat;
19.10
19.11 fun thms_containing_consts thy consts =
20.1 --- a/src/Pure/sign.ML Tue Sep 20 08:20:22 2005 +0200
20.2 +++ b/src/Pure/sign.ML Tue Sep 20 08:21:49 2005 +0200
20.3 @@ -227,7 +227,7 @@
20.4 val naming = NameSpace.default_naming;
20.5 val syn = Syntax.merge_syntaxes syn1 syn2;
20.6 val tsig = Type.merge_tsigs pp (tsig1, tsig2);
20.7 - val consts = NameSpace.merge_tables eq_snd (consts1, consts2)
20.8 + val consts = NameSpace.merge_tables (eq_snd (op =)) (consts1, consts2)
20.9 handle Symtab.DUPS cs => err_dup_consts cs;
20.10 val constraints = Symtab.merge (op =) (constraints1, constraints2)
20.11 handle Symtab.DUPS cs => err_inconsistent_constraints cs;
21.1 --- a/src/Pure/tactic.ML Tue Sep 20 08:20:22 2005 +0200
21.2 +++ b/src/Pure/tactic.ML Tue Sep 20 08:21:49 2005 +0200
21.3 @@ -573,9 +573,9 @@
21.4 (*folding should handle critical pairs! E.g. K == Inl(0), S == Inr(Inl(0))
21.5 Returns longest lhs first to avoid folding its subexpressions.*)
21.6 fun sort_lhs_depths defs =
21.7 - let val keylist = make_keylist (term_depth o lhs_of_thm) defs
21.8 + let val keylist = AList.make (term_depth o lhs_of_thm) defs
21.9 val keys = distinct (sort (rev_order o int_ord) (map #2 keylist))
21.10 - in map (keyfilter keylist) keys end;
21.11 + in map (AList.find (op =) keylist) keys end;
21.12
21.13 val rev_defs = sort_lhs_depths o map symmetric;
21.14
22.1 --- a/src/Pure/theory.ML Tue Sep 20 08:20:22 2005 +0200
22.2 +++ b/src/Pure/theory.ML Tue Sep 20 08:21:49 2005 +0200
22.3 @@ -120,7 +120,7 @@
22.4
22.5 val axioms = NameSpace.empty_table;
22.6 val defs = Defs.merge pp defs1 defs2;
22.7 - val oracles = NameSpace.merge_tables eq_snd (oracles1, oracles2)
22.8 + val oracles = NameSpace.merge_tables (eq_snd (op =)) (oracles1, oracles2)
22.9 handle Symtab.DUPS dups => err_dup_oras dups;
22.10 in make_thy (axioms, defs, oracles) end;
22.11
23.1 --- a/src/Pure/type.ML Tue Sep 20 08:20:22 2005 +0200
23.2 +++ b/src/Pure/type.ML Tue Sep 20 08:21:49 2005 +0200
23.3 @@ -632,7 +632,7 @@
23.4 fun add_nonterminals naming = change_types o fold (new_decl naming) o map (rpair Nonterminal);
23.5
23.6 fun merge_types (types1, types2) =
23.7 - NameSpace.merge_tables Library.eq_snd (types1, types2) handle Symtab.DUPS (d :: _) =>
23.8 + NameSpace.merge_tables (Library.eq_snd (op =)) (types1, types2) handle Symtab.DUPS (d :: _) =>
23.9 err_in_decls d (the_decl types1 d) (the_decl types2 d);
23.10
23.11 end;
24.1 --- a/src/Pure/type_infer.ML Tue Sep 20 08:20:22 2005 +0200
24.2 +++ b/src/Pure/type_infer.ML Tue Sep 20 08:21:49 2005 +0200
24.3 @@ -452,7 +452,7 @@
24.4 xi = xi' andalso Type.eq_sort tsig (S, S');
24.5
24.6 val env = gen_distinct eq (map (apsnd map_sort) raw_env);
24.7 - val _ = (case gen_duplicates eq_fst env of [] => ()
24.8 + val _ = (case gen_duplicates (eq_fst (op =)) env of [] => ()
24.9 | dups => error ("Inconsistent sort constraints for type variable(s) "
24.10 ^ commas_quote (map (Syntax.string_of_vname' o fst) dups)));
24.11