# HG changeset patch # User haftmann # Date 1127197309 -7200 # Node ID 26535df536ae0b6d236e391e41d129f37c2915d8 # Parent ddb14cbec6a24b27d50dda1d41ef0a6f1bd3c3c8 slight adaptions to library changes diff -r ddb14cbec6a2 -r 26535df536ae src/CTT/CTT.ML --- 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 diff -r ddb14cbec6a2 -r 26535df536ae src/CTT/rew.ML --- 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); diff -r ddb14cbec6a2 -r 26535df536ae src/FOL/intprover.ML --- 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, diff -r ddb14cbec6a2 -r 26535df536ae src/FOLP/classical.ML --- 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, diff -r ddb14cbec6a2 -r 26535df536ae src/FOLP/intprover.ML --- 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, diff -r ddb14cbec6a2 -r 26535df536ae src/HOL/Tools/recdef_package.ML --- 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 []; diff -r ddb14cbec6a2 -r 26535df536ae src/Provers/Arith/fast_lin_arith.ML --- 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 () diff -r ddb14cbec6a2 -r 26535df536ae src/Pure/Isar/attrib.ML --- 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 = diff -r ddb14cbec6a2 -r 26535df536ae src/Pure/Isar/context_rules.ML --- 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); diff -r ddb14cbec6a2 -r 26535df536ae src/Pure/Isar/locale.ML --- 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); diff -r ddb14cbec6a2 -r 26535df536ae src/Pure/Isar/method.ML --- 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 = diff -r ddb14cbec6a2 -r 26535df536ae src/Pure/Isar/proof_context.ML --- 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 *) diff -r ddb14cbec6a2 -r 26535df536ae src/Pure/Isar/term_style.ML --- 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); diff -r ddb14cbec6a2 -r 26535df536ae src/Pure/Syntax/syntax.ML --- 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))) diff -r ddb14cbec6a2 -r 26535df536ae src/Pure/Thy/present.ML --- 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); diff -r ddb14cbec6a2 -r 26535df536ae src/Pure/Thy/thy_parse.ML --- 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 () diff -r ddb14cbec6a2 -r 26535df536ae src/Pure/axclass.ML --- 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; diff -r ddb14cbec6a2 -r 26535df536ae src/Pure/meta_simplifier.ML --- 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 diff -r ddb14cbec6a2 -r 26535df536ae src/Pure/pure_thy.ML --- 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 = diff -r ddb14cbec6a2 -r 26535df536ae src/Pure/sign.ML --- 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; diff -r ddb14cbec6a2 -r 26535df536ae src/Pure/tactic.ML --- 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; diff -r ddb14cbec6a2 -r 26535df536ae src/Pure/theory.ML --- 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; diff -r ddb14cbec6a2 -r 26535df536ae src/Pure/type.ML --- 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; diff -r ddb14cbec6a2 -r 26535df536ae src/Pure/type_infer.ML --- 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)));