# HG changeset patch # User wenzelm # Date 1417028734 -3600 # Node ID a78612c67ec021e985fd6aeb09fcb87f13e1d5ee # Parent 5b649fb2f2e10046a11607a6c29353e6015f3c3f renamed "pairself" to "apply2", in accordance to @{apply 2}; diff -r 5b649fb2f2e1 -r a78612c67ec0 NEWS --- a/NEWS Wed Nov 26 16:55:43 2014 +0100 +++ b/NEWS Wed Nov 26 20:05:34 2014 +0100 @@ -224,6 +224,9 @@ available as parameterized antiquotations, e.g. @{map 4} for lists of quadruples. +* Renamed "pairself" to "apply2", in accordance to @{apply 2}. +INCOMPATIBILITY. + *** System *** diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Decision_Procs/Approximation.thy --- a/src/HOL/Decision_Procs/Approximation.thy Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Decision_Procs/Approximation.thy Wed Nov 26 20:05:34 2014 +0100 @@ -3502,7 +3502,7 @@ fun term_of_float_float_option NONE = @{term "None :: (float \ float) option"} | term_of_float_float_option (SOME ff) = @{term "Some :: float \ float \ _"} - $ HOLogic.mk_prod (pairself term_of_float ff); + $ HOLogic.mk_prod (apply2 term_of_float ff); val term_of_float_float_option_list = HOLogic.mk_list @{typ "(float \ float) option"} o map term_of_float_float_option; @@ -3551,7 +3551,7 @@ fun float_float_option_of_term @{term "None :: (float \ float) option"} = NONE | float_float_option_of_term (@{term "Some :: float \ float \ _"} $ ff) = - SOME (pairself float_of_term (HOLogic.dest_prod ff)) + SOME (apply2 float_of_term (HOLogic.dest_prod ff)) | float_float_option_of_term (@{term approx'} $ n $ a $ ffs) = @{code approx'} (nat_of_term n) (floatarith_of_term a) (float_float_option_list_of_term ffs) | float_float_option_of_term t = bad t diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Wed Nov 26 20:05:34 2014 +0100 @@ -4006,7 +4006,7 @@ fun binopT T = T --> T --> T; fun relT T = T --> T --> @{typ bool}; -val mk_C = @{code C} o pairself @{code int_of_integer}; +val mk_C = @{code C} o apply2 @{code int_of_integer}; val mk_poly_Bound = @{code poly.Bound} o @{code nat_of_integer}; val mk_Bound = @{code Bound} o @{code nat_of_integer}; @@ -4082,7 +4082,7 @@ fun term_of_num T ps (@{code poly.C} (a, b)) = let - val (c, d) = pairself (@{code integer_of_int}) (a, b) + val (c, d) = apply2 (@{code integer_of_int}) (a, b) in (if d = 1 then HOLogic.mk_number T c else if d = 0 then Const (@{const_name Groups.zero}, T) diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Decision_Procs/ferrante_rackoff.ML --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Wed Nov 26 20:05:34 2014 +0100 @@ -57,7 +57,7 @@ val ((p1_v,p2_v),(mp1_v,mp2_v)) = funpow 2 (Thm.dest_arg o snd o Thm.dest_abs NONE) (funpow 4 Thm.dest_arg (cprop_of (hd minf))) - |> Thm.dest_binop |> pairself Thm.dest_binop |> apfst (pairself Thm.dest_fun) + |> Thm.dest_binop |> apply2 Thm.dest_binop |> apfst (apply2 Thm.dest_fun) fun myfwd (th1, th2, th3, th4, th5) p1 p2 [(th_1,th_2,th_3,th_4,th_5), (th_1',th_2',th_3',th_4',th_5')] = diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Divides.thy Wed Nov 26 20:05:34 2014 +0100 @@ -2104,20 +2104,23 @@ fun binary_proc proc ctxt ct = (case Thm.term_of ct of _ $ t $ u => - (case try (pairself (`(snd o HOLogic.dest_number))) (t, u) of + (case try (apply2 (`(snd o HOLogic.dest_number))) (t, u) of SOME args => proc ctxt args | NONE => NONE) | _ => NONE); in fun divmod_proc posrule negrule = binary_proc (fn ctxt => fn ((a, t), (b, u)) => - if b = 0 then NONE else let - val (q, r) = pairself mk_number (Integer.div_mod a b) - val goal1 = HOLogic.mk_eq (t, plus $ (times $ u $ q) $ r) - val (goal2, goal3, rule) = if b > 0 - then (le $ zero $ r, less $ r $ u, posrule RS eq_reflection) - else (le $ r $ zero, less $ u $ r, negrule RS eq_reflection) - in SOME (rule OF map (prove ctxt) [goal1, goal2, goal3]) end) + if b = 0 then NONE + else + let + val (q, r) = apply2 mk_number (Integer.div_mod a b) + val goal1 = HOLogic.mk_eq (t, plus $ (times $ u $ q) $ r) + val (goal2, goal3, rule) = + if b > 0 + then (le $ zero $ r, less $ r $ u, posrule RS eq_reflection) + else (le $ r $ zero, less $ u $ r, negrule RS eq_reflection) + in SOME (rule OF map (prove ctxt) [goal1, goal2, goal3]) end) end *} diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/HOLCF/Tools/Domain/domain_constructors.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Wed Nov 26 20:05:34 2014 +0100 @@ -344,7 +344,7 @@ fun dist_le (con1, args1) (con2, args2) = let val (vs1, zs1) = get_vars args1 - val (vs2, _) = get_vars args2 |> pairself (map prime) + val (vs2, _) = get_vars args2 |> apply2 (map prime) val lhs = mk_below (list_ccomb (con1, vs1), list_ccomb (con2, vs2)) val rhss = map mk_undef zs1 val goal = mk_trp (iff_disj (lhs, rhss)) @@ -355,7 +355,7 @@ fun dist_eq (con1, args1) (con2, args2) = let val (vs1, zs1) = get_vars args1 - val (vs2, zs2) = get_vars args2 |> pairself (map prime) + val (vs2, zs2) = get_vars args2 |> apply2 (map prime) val lhs = mk_eq (list_ccomb (con1, vs1), list_ccomb (con2, vs2)) val rhss1 = map mk_undef zs1 val rhss2 = map mk_undef zs2 diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/HOLCF/Tools/fixrec.ML --- a/src/HOL/HOLCF/Tools/fixrec.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/HOLCF/Tools/fixrec.ML Wed Nov 26 20:05:34 2014 +0100 @@ -274,7 +274,7 @@ | [] => fixrec_err "no defining equations for function" | _ => fixrec_err "all equations in block must define the same function" val vars = - case distinct (op = o pairself length) (map fst matchers) of + case distinct (op = o apply2 length) (map fst matchers) of [vars] => vars | _ => fixrec_err "all equations in block must have the same arity" (* rename so all matchers use same free variables *) diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Hoare/hoare_syntax.ML --- a/src/HOL/Hoare/hoare_syntax.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Hoare/hoare_syntax.ML Wed Nov 26 20:05:34 2014 +0100 @@ -22,7 +22,7 @@ | idt_name _ = NONE; fun eq_idt tu = - (case pairself idt_name tu of + (case apply2 idt_name tu of (SOME x, SOME y) => x = y | _ => false); diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Imperative_HOL/Heap_Monad.thy --- a/src/HOL/Imperative_HOL/Heap_Monad.thy Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Wed Nov 26 20:05:34 2014 +0100 @@ -691,7 +691,7 @@ | imp_monad_bind (v_ty `|=> t) = v_ty `|=> imp_monad_bind t | imp_monad_bind (ICase { term = t, typ = ty, clauses = clauses, primitive = t0 }) = ICase { term = imp_monad_bind t, typ = ty, - clauses = (map o pairself) imp_monad_bind clauses, primitive = imp_monad_bind t0 }; + clauses = (map o apply2) imp_monad_bind clauses, primitive = imp_monad_bind t0 }; in (Code_Symbol.Graph.map o K o map_terms_stmt) imp_monad_bind end; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Library/Old_SMT/old_smt_normalize.ML --- a/src/HOL/Library/Old_SMT/old_smt_normalize.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Library/Old_SMT/old_smt_normalize.ML Wed Nov 26 20:05:34 2014 +0100 @@ -185,7 +185,7 @@ if has_all_vars vs (Thm.term_of ct) then (case Thm.term_of ct of _ $ _ => - (case pairself (minimal_pats vs) (Thm.dest_comb ct) of + (case apply2 (minimal_pats vs) (Thm.dest_comb ct) of ([], []) => [[ct]] | (ctss, ctss') => union (eq_set (op aconvc)) ctss ctss') | _ => []) @@ -203,7 +203,7 @@ Old_SMT_Utils.mk_const_pat @{theory} @{const_name pat} Old_SMT_Utils.destT1 fun mk_pat ct = Thm.apply (Old_SMT_Utils.instT' ct pat) ct - fun mk_clist T = pairself (Thm.cterm_of @{theory}) + fun mk_clist T = apply2 (Thm.cterm_of @{theory}) (HOLogic.cons_const T, HOLogic.nil_const T) fun mk_list (ccons, cnil) f cts = fold_rev (Thm.mk_binop ccons o f) cts cnil val mk_pat_list = mk_list (mk_clist @{typ pattern}) diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Library/Old_SMT/old_z3_model.ML --- a/src/HOL/Library/Old_SMT/old_z3_model.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Library/Old_SMT/old_z3_model.ML Wed Nov 26 20:05:34 2014 +0100 @@ -225,7 +225,7 @@ SOME (@{const of_nat (int)}, _) => true | SOME (@{const nat}, _) => true | _ => false) - in pairself (replace_vars nats) (eqs', filter_out is_coercion defs) end + in apply2 (replace_vars nats) (eqs', filter_out is_coercion defs) end fun unfold_funapp (eqs, defs) = let @@ -263,13 +263,13 @@ fun unfold_vars (es, ds) = (case first_eq rewr_var es of - SOME (lr, es') => unfold_vars (pairself (replace lr) (es', ds)) + SOME (lr, es') => unfold_vars (apply2 (replace lr) (es', ds)) | NONE => (es, ds)) fun unfold_frees ues (es, ds) = (case first_eq rewr_free es of SOME (lr, es') => - pairself (replace lr) (es', ds) + apply2 (replace lr) (es', ds) |> unfold_frees (HOLogic.mk_eq lr :: replace lr ues) | NONE => (ues @ es, ds)) @@ -310,7 +310,7 @@ | is_free_def _ = false fun defined tp = - try (pairself (fst o HOLogic.dest_eq)) tp + try (apply2 (fst o HOLogic.dest_eq)) tp |> the_default false o Option.map (op aconv) fun add_free_defs free_cs defs = diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Library/Old_SMT/old_z3_proof_literals.ML --- a/src/HOL/Library/Old_SMT/old_z3_proof_literals.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_literals.ML Wed Nov 26 20:05:34 2014 +0100 @@ -262,7 +262,7 @@ | NONE => (case lookup_rule t of (rewrite, SOME lit) => (s, rewrite lit) - | (_, NONE) => (s, comp (pairself join1 (dest t))))) + | (_, NONE) => (s, comp (apply2 join1 (dest t))))) in snd (join1 (if is_conj then (false, t) else (true, t))) end @@ -299,7 +299,7 @@ SOME rs => extract_lit thm rs | NONE => the (Termtab.get_first contra_lits rules) - |> pairself (extract_lit thm) + |> apply2 (extract_lit thm) |> (fn (nlit, plit) => nlit COMP (plit COMP contra_rule))) end diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Library/Old_SMT/old_z3_proof_methods.ML --- a/src/HOL/Library/Old_SMT/old_z3_proof_methods.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_methods.ML Wed Nov 26 20:05:34 2014 +0100 @@ -115,7 +115,7 @@ fun prove_inj_eq ctxt ct = let val (lhs, rhs) = - pairself Old_SMT_Utils.mk_cprop (Thm.dest_binop (Old_SMT_Utils.dest_cprop ct)) + apply2 Old_SMT_Utils.mk_cprop (Thm.dest_binop (Old_SMT_Utils.dest_cprop ct)) val lhs_thm = Thm.implies_intr rhs (prove_lhs ctxt rhs lhs) val rhs_thm = Thm.implies_intr lhs (prove_rhs ctxt (mk_inv_def ctxt rhs) lhs rhs) @@ -126,7 +126,7 @@ val swap_disj_thm = mk_meta_eq @{thm disj_commute} fun swap_conv dest eq = - Old_SMT_Utils.if_true_conv ((op <) o pairself Term.size_of_term o dest) + Old_SMT_Utils.if_true_conv ((op <) o apply2 Term.size_of_term o dest) (Conv.rewr_conv eq) val swap_eq_conv = swap_conv HOLogic.dest_eq swap_eq_thm diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML --- a/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML Wed Nov 26 20:05:34 2014 +0100 @@ -287,7 +287,7 @@ end fun dest_arg2 ct = Thm.dest_arg (Thm.dest_arg ct) - fun dest ct = pairself dest_arg2 (Thm.dest_binop ct) + fun dest ct = apply2 dest_arg2 (Thm.dest_binop ct) val contrapos = Old_Z3_Proof_Tools.precompose2 dest @{lemma "(~P ==> ~Q) ==> Q ==> P" by fast} in @@ -482,7 +482,7 @@ fun prove_refl (ct, _) = Thm.reflexive ct fun prove_comb f g cp = - let val ((ct1, ct2), (cu1, cu2)) = pairself Thm.dest_comb cp + let val ((ct1, ct2), (cu1, cu2)) = apply2 Thm.dest_comb cp in Thm.combination (f (ct1, cu1)) (g (ct2, cu2)) end fun prove_arg f = prove_comb prove_refl f @@ -506,7 +506,7 @@ fun prove_distinct f = prove_arg (with_length (prove_list f)) fun prove_eq exn lookup cp = - (case lookup (Logic.mk_equals (pairself Thm.term_of cp)) of + (case lookup (Logic.mk_equals (apply2 Thm.term_of cp)) of SOME eq => eq | NONE => if exn then raise MONO else prove_refl cp) diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Library/Sum_of_Squares/sum_of_squares.ML --- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Wed Nov 26 20:05:34 2014 +0100 @@ -575,7 +575,7 @@ Inttriplefunc.fold (fn ((b, i, j), c) => fn a => if i > j then a else ((b, i, j), c) :: a) m [] - val entss = sort (triple_int_ord o pairself fst) ents + val entss = sort (triple_int_ord o apply2 fst) ents in fold_rev (fn ((b,i,j),c) => fn a => pfx ^ string_of_int b ^ " " ^ string_of_int i ^ " " ^ string_of_int j ^ diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Library/positivstellensatz.ML --- a/src/HOL/Library/positivstellensatz.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Library/positivstellensatz.ML Wed Nov 26 20:05:34 2014 +0100 @@ -64,13 +64,13 @@ structure Symfunc = FuncFun(type key = string val ord = fast_string_ord); structure Termfunc = FuncFun(type key = term val ord = Term_Ord.fast_term_ord); -val cterm_ord = Term_Ord.fast_term_ord o pairself term_of +val cterm_ord = Term_Ord.fast_term_ord o apply2 term_of structure Ctermfunc = FuncFun(type key = cterm val ord = cterm_ord); type monomial = int Ctermfunc.table; -val monomial_ord = list_ord (prod_ord cterm_ord int_ord) o pairself Ctermfunc.dest +val monomial_ord = list_ord (prod_ord cterm_ord int_ord) o apply2 Ctermfunc.dest structure Monomialfunc = FuncFun(type key = monomial val ord = monomial_ord) @@ -78,7 +78,7 @@ (* The ordering so we can create canonical HOL polynomials. *) -fun dest_monomial mon = sort (cterm_ord o pairself fst) (Ctermfunc.dest mon); +fun dest_monomial mon = sort (cterm_ord o apply2 fst) (Ctermfunc.dest mon); fun monomial_order (m1,m2) = if Ctermfunc.is_empty m2 then LESS diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Matrix_LP/FloatSparseMatrixBuilder.ML --- a/src/HOL/Matrix_LP/FloatSparseMatrixBuilder.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Matrix_LP/FloatSparseMatrixBuilder.ML Wed Nov 26 20:05:34 2014 +0100 @@ -80,7 +80,7 @@ val eupper = HOLogic.mk_prod (index, fupper) in (elower :: lower, eupper :: upper) end; in - pairself (HOLogic.mk_list spvec_elemT) (Inttab.fold app vector ([], [])) + apply2 (HOLogic.mk_list spvec_elemT) (Inttab.fold app vector ([], [])) end; fun approx_matrix prec pprt vector = @@ -93,7 +93,7 @@ val eupper = HOLogic.mk_prod (index, fupper) in (elower :: lower, eupper :: upper) end; in - pairself (HOLogic.mk_list spmat_elemT) (Inttab.fold app vector ([], [])) + apply2 (HOLogic.mk_list spmat_elemT) (Inttab.fold app vector ([], [])) end; exception Nat_expected of int; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Matrix_LP/float_arith.ML --- a/src/HOL/Matrix_LP/float_arith.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Matrix_LP/float_arith.ML Wed Nov 26 20:05:34 2014 +0100 @@ -204,10 +204,10 @@ end fun mk_float (a, b) = @{term "float"} $ - HOLogic.mk_prod (pairself (HOLogic.mk_number HOLogic.intT) (a, b)); + HOLogic.mk_prod (apply2 (HOLogic.mk_number HOLogic.intT) (a, b)); fun dest_float (Const (@{const_name float}, _) $ (Const (@{const_name Pair}, _) $ a $ b)) = - pairself (snd o HOLogic.dest_number) (a, b) + apply2 (snd o HOLogic.dest_number) (a, b) | dest_float t = ((snd o HOLogic.dest_number) t, 0); fun approx_float prec f value = diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Wed Nov 26 20:05:34 2014 +0100 @@ -57,7 +57,7 @@ fun do_line line = (case line |> space_explode ":" of [line_num, offset, proof] => - SOME (pairself (the o Int.fromString) (line_num, offset), + SOME (apply2 (the o Int.fromString) (line_num, offset), proof |> space_explode " " |> filter_out (curry (op =) "")) | _ => NONE) val proofs = File.read (Path.explode proof_file) diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Nitpick_Examples/Mono_Nits.thy --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Wed Nov 26 20:05:34 2014 +0100 @@ -153,7 +153,7 @@ fun theorems_of thy = filter (fn (name, th) => not (is_forbidden_theorem name) andalso - (theory_of_thm th, thy) |> pairself Context.theory_name |> op =) + (theory_of_thm th, thy) |> apply2 Context.theory_name |> op =) (Global_Theory.all_thms_of thy true) fun check_formulas tsp = diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Nitpick_Examples/minipick.ML --- a/src/HOL/Nitpick_Examples/minipick.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Nitpick_Examples/minipick.ML Wed Nov 26 20:05:34 2014 +0100 @@ -123,7 +123,7 @@ if pos andalso not (concrete T) then False else - (t1, t2) |> pairself (to_R_rep Ts) + (t1, t2) |> apply2 (to_R_rep Ts) |> (if pos then Some o Intersect else Lone o Union) and to_F pos Ts t = (case t of diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Nominal/nominal_datatype.ML Wed Nov 26 20:05:34 2014 +0100 @@ -1664,7 +1664,7 @@ (rec_unique_frees ~~ rec_result_Ts ~~ rec_sets); val induct_aux_rec = Drule.cterm_instantiate - (map (pairself (cterm_of thy11) o apsnd (augment_sort thy11 fs_cp_sort)) + (map (apply2 (cterm_of thy11) o apsnd (augment_sort thy11 fs_cp_sort)) (map (fn (aT, f) => (Logic.varify_global f, Abs ("z", HOLogic.unitT, Const (@{const_name Nominal.supp}, fun_tupleT --> HOLogic.mk_setT aT) $ fun_tuple))) fresh_fs @ diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Nominal/nominal_fresh_fun.ML --- a/src/HOL/Nominal/nominal_fresh_fun.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML Wed Nov 26 20:05:34 2014 +0100 @@ -23,8 +23,8 @@ (head_of (Logic.incr_indexes (Ts, j) t), fold_rev Term.abs ps u)) tinst; val th' = instf - (map (pairself (ctyp_of thy)) tyinst') - (map (pairself (cterm_of thy)) tinst') + (map (apply2 (ctyp_of thy)) tyinst') + (map (apply2 (cterm_of thy)) tinst') (Thm.lift_rule cgoal th) in compose_tac ctxt (elim, th', nprems_of th) i st diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Nominal/nominal_induct.ML --- a/src/HOL/Nominal/nominal_induct.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Nominal/nominal_induct.ML Wed Nov 26 20:05:34 2014 +0100 @@ -54,7 +54,7 @@ end; val substs = map2 subst insts concls |> flat |> distinct (op =) - |> map (pairself (Thm.cterm_of (Proof_Context.theory_of ctxt))); + |> map (apply2 (Thm.cterm_of (Proof_Context.theory_of ctxt))); in (((cases, nconcls), consumes), Drule.cterm_instantiate substs joined_rule) end; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Nominal/nominal_inductive.ML Wed Nov 26 20:05:34 2014 +0100 @@ -62,7 +62,7 @@ in (add_binders thy i u (fold (fn (u, T) => if exists (fn j => j < i) (loose_bnos u) then I - else insert (op aconv o pairself fst) + else insert (op aconv o apply2 fst) (incr_boundvars (~i) u, T)) cargs1 bs'), cargs2) end) cargs (bs, ts ~~ Ts)))) | _ => fold (add_binders thy i) ts bs) @@ -164,7 +164,7 @@ HOLogic.dest_conj |> map (HOLogic.dest_imp ##> strip_comb); val ps = map (fst o snd) concls; - val _ = (case duplicates (op = o pairself fst) avoids of + val _ = (case duplicates (op = o apply2 fst) avoids of [] => () | xs => error ("Duplicate case names: " ^ commas_quote (map fst xs))); val _ = avoids |> forall (fn (a, xs) => null (duplicates (op =) xs) orelse @@ -338,7 +338,7 @@ val pis'' = fold (concat_perm #> map) pis' pis; val env = Pattern.first_order_match thy (ihypt, prop_of ihyp) (Vartab.empty, Vartab.empty); - val ihyp' = Thm.instantiate ([], map (pairself (cterm_of thy)) + val ihyp' = Thm.instantiate ([], map (apply2 (cterm_of thy)) (map (Envir.subst_term env) vs ~~ map (fold_rev (NominalDatatype.mk_perm []) (rev pis' @ pis)) params' @ [z])) ihyp; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Nominal/nominal_inductive2.ML Wed Nov 26 20:05:34 2014 +0100 @@ -173,7 +173,7 @@ HOLogic.dest_conj |> map (HOLogic.dest_imp ##> strip_comb); val ps = map (fst o snd) concls; - val _ = (case duplicates (op = o pairself fst) avoids of + val _ = (case duplicates (op = o apply2 fst) avoids of [] => () | xs => error ("Duplicate case names: " ^ commas_quote (map fst xs))); val _ = (case subtract (op =) induct_cases (map fst avoids) of diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Random.thy --- a/src/HOL/Random.thy Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Random.thy Wed Nov 26 20:05:34 2014 +0100 @@ -156,7 +156,7 @@ val now = Time.toMilliseconds (Time.now ()); val (q, s1) = IntInf.divMod (now, 2147483562); val s2 = q mod 2147483398; - in pairself Code_Numeral.natural_of_integer (s1 + 1, s2 + 1) end); + in apply2 Code_Numeral.natural_of_integer (s1 + 1, s2 + 1) end); in diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/SPARK/Tools/spark_vcs.ML --- a/src/HOL/SPARK/Tools/spark_vcs.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML Wed Nov 26 20:05:34 2014 +0100 @@ -33,10 +33,10 @@ fun err_unfinished () = error "An unfinished SPARK environment is still open." -val strip_number = pairself implode o take_suffix Fdl_Lexer.is_digit o raw_explode; +val strip_number = apply2 implode o take_suffix Fdl_Lexer.is_digit o raw_explode; val name_ord = prod_ord string_ord (option_ord int_ord) o - pairself (strip_number ##> Int.fromString); + apply2 (strip_number ##> Int.fromString); structure VCtab = Table(type key = string val ord = name_ord); @@ -72,7 +72,7 @@ val to_lower = raw_explode #> map Symbol.to_ascii_lower #> implode; -val lcase_eq = (op =) o pairself (to_lower o Long_Name.base_name); +val lcase_eq = (op =) o apply2 (to_lower o Long_Name.base_name); fun lookup_prfx "" tab s = Symtab.lookup tab s | lookup_prfx prfx tab s = (case Symtab.lookup tab s of @@ -366,7 +366,7 @@ | SOME {fields, ...} => let val fields' = invert_map cmap fields in - (case subtract (lcase_eq o pairself fst) fldTs fields' of + (case subtract (lcase_eq o apply2 fst) fldTs fields' of [] => () | flds => assoc_ty_err thy rT s ("has extra field(s) " ^ commas (map (Long_Name.base_name o fst) flds)); @@ -862,8 +862,8 @@ fun check_mapping _ _ [] _ = () | check_mapping err s cmap cs = - (case duplicates (op = o pairself fst) cmap of - [] => (case duplicates (op = o pairself snd) cmap of + (case duplicates (op = o apply2 fst) cmap of + [] => (case duplicates (op = o apply2 snd) cmap of [] => (case subtract (op = o apsnd snd) cs cmap of [] => (case subtract (op = o apfst snd) cmap cs of [] => () diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML --- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Wed Nov 26 20:05:34 2014 +0100 @@ -574,14 +574,14 @@ diff thy (scheme_t, instance_t) (*valuation of type variables*) - val typeval = map (pairself (ctyp_of thy)) type_pairing + val typeval = map (apply2 (ctyp_of thy)) type_pairing val typeval_env = map (apfst dest_TVar) type_pairing (*valuation of term variables*) val termval = map (apfst (type_devar typeval_env)) term_pairing - |> map (pairself (cterm_of thy)) + |> map (apply2 (cterm_of thy)) in Thm.instantiate (typeval, termval) scheme_thm end diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/TPTP/atp_problem_import.ML --- a/src/HOL/TPTP/atp_problem_import.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/TPTP/atp_problem_import.ML Wed Nov 26 20:05:34 2014 +0100 @@ -56,7 +56,7 @@ ||> List.partition (has_role TPTP_Syntax.Role_Definition) in (map (get_prop I) conjs, - pairself (map (get_prop Logic.varify_global)) defs_and_nondefs, + apply2 (map (get_prop Logic.varify_global)) defs_and_nondefs, Named_Target.theory_init thy) end diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/TPTP/atp_theory_export.ML Wed Nov 26 20:05:34 2014 +0100 @@ -127,7 +127,7 @@ | ident_of_problem_line (Class_Memb (ident, _, _, _)) = ident | ident_of_problem_line (Formula ((ident, _), _, _, _, _)) = ident -fun order_facts ord = sort (ord o pairself ident_of_problem_line) +fun order_facts ord = sort (ord o apply2 ident_of_problem_line) fun order_problem_facts _ [] = [] | order_problem_facts ord ((heading, lines) :: problem) = @@ -166,7 +166,7 @@ val facts = Sledgehammer_Fact.all_facts (Proof_Context.init_global thy) true false Keyword.empty_keywords [] [] css_table - |> sort (Sledgehammer_MaSh.crude_thm_ord o pairself snd) + |> sort (Sledgehammer_MaSh.crude_thm_ord o apply2 snd) val problem = facts |> map (fn ((_, loc), th) => @@ -202,7 +202,7 @@ val order_tab = Symtab.empty |> fold (Symtab.insert (op =)) (ordered_names ~~ (1 upto length ordered_names)) - val name_ord = int_ord o pairself (the o Symtab.lookup order_tab) + val name_ord = int_ord o apply2 (the o Symtab.lookup order_tab) in problem |> (case format of @@ -297,7 +297,7 @@ problem_of_theory ctxt thy format infer_policy type_enc |> split_last ||> (snd - #> chop_maximal_groups (op = o pairself theory_name_of_fact) + #> chop_maximal_groups (op = o apply2 theory_name_of_fact) #> map (`(include_base_name_of_fact o hd))) fun write_prelude () = let val ss = lines_of_problem ctxt format prelude in diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/TPTP/mash_eval.ML --- a/src/HOL/TPTP/mash_eval.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/TPTP/mash_eval.ML Wed Nov 26 20:05:34 2014 +0100 @@ -66,7 +66,7 @@ (if is_none outcome then "Success (" ^ ATP_Util.string_of_time run_time ^ "): " ^ (used_facts |> map (with_index facts o fst) - |> sort (int_ord o pairself fst) + |> sort (int_ord o apply2 fst) |> map index_str |> space_implode " ") ^ (if length facts < the max_facts then diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/TPTP/mash_export.ML Wed Nov 26 20:05:34 2014 +0100 @@ -65,7 +65,7 @@ fun all_facts ctxt = let val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt in Sledgehammer_Fact.all_facts ctxt true false Keyword.empty_keywords [] [] css - |> sort (crude_thm_ord o pairself snd) + |> sort (crude_thm_ord o apply2 snd) end fun filter_accessible_from th = filter (fn (_, th') => thm_less (th', th)) diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/ATP/atp_problem.ML Wed Nov 26 20:05:34 2014 +0100 @@ -304,7 +304,7 @@ | raw_polarities_of_conn AIff = (NONE, NONE) fun polarities_of_conn NONE = K (NONE, NONE) | polarities_of_conn (SOME pos) = - raw_polarities_of_conn #> not pos ? pairself (Option.map not) + raw_polarities_of_conn #> not pos ? apply2 (Option.map not) fun mk_anot (AConn (ANot, [phi])) = phi | mk_anot phi = AConn (ANot, [phi]) @@ -776,10 +776,10 @@ fun clausify_formula pos (phi as AAtom _) = [phi |> not pos ? mk_anot] | clausify_formula pos (AConn (ANot, [phi])) = clausify_formula (not pos) phi | clausify_formula true (AConn (AOr, [phi1, phi2])) = - (phi1, phi2) |> pairself (clausify_formula true) + (phi1, phi2) |> apply2 (clausify_formula true) |> uncurry (map_product (mk_aconn AOr)) | clausify_formula false (AConn (AAnd, [phi1, phi2])) = - (phi1, phi2) |> pairself (clausify_formula false) + (phi1, phi2) |> apply2 (clausify_formula false) |> uncurry (map_product (mk_aconn AOr)) | clausify_formula true (AConn (AImplies, [phi1, phi2])) = clausify_formula true (AConn (AOr, [mk_anot phi1, phi2])) diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Nov 26 20:05:34 2014 +0100 @@ -789,8 +789,8 @@ (facts, lifted) (* Lambda-lifting sometimes leaves some lambdas around; we need some way to get rid of them *) - |> pairself (map (introduce_combinators ctxt)) - |> pairself (map constify_lifted) + |> apply2 (map (introduce_combinators ctxt)) + |> apply2 (map constify_lifted) (* Requires bound variables not to clash with any schematic variables (as should be the case right after lambda-lifting). *) |>> map (hol_open_form (unprefix hol_close_form_prefix)) @@ -1317,7 +1317,7 @@ [] else 0 upto length footprint - 1 ~~ footprint - |> sort (rev_order o list_ord Term_Ord.indexname_ord o pairself snd) + |> sort (rev_order o list_ord Term_Ord.indexname_ord o apply2 snd) |> cover [] end @@ -1752,7 +1752,7 @@ ths ~~ (1 upto length ths) |> maps (dub_and_inst needs_sound o apfst (apsnd prop_of)) |> make_facts - |> union (op = o pairself #iformula)) + |> union (op = o apply2 #iformula)) (if completish then completish_helper_table else helper_table) end | NONE => I) @@ -1860,7 +1860,7 @@ |> map2 (pair o rpair (Local, General) o string_of_int) (0 upto length hyp_ts) val ((conjs, facts), lam_facts) = (conjs, facts) - |> presimp ? pairself (map (apsnd (apsnd (presimp_prop ctxt type_enc)))) + |> presimp ? apply2 (map (apsnd (apsnd (presimp_prop ctxt type_enc)))) |> (if lam_trans = no_lamsN then rpair [] else @@ -2604,7 +2604,7 @@ fun firstorderize in_helper = firstorderize_fact thy ctrss type_enc (uncurried_aliases andalso not in_helper) completish sym_tab0 - val (conjs, facts) = (conjs, facts) |> pairself (map (firstorderize false)) + val (conjs, facts) = (conjs, facts) |> apply2 (map (firstorderize false)) val (ho_stuff, sym_tab) = sym_table_of_facts ctxt type_enc Min_App_Op conjs facts val (uncurried_alias_eq_tms, uncurried_alias_eq_lines) = @@ -2705,7 +2705,7 @@ |> fold (fold (add_line_weights type_info_default_weight) o get) [explicit_declsN, subclassesN, tconsN] |> Symtab.dest - |> sort (prod_ord Real.compare string_ord o pairself swap) + |> sort (prod_ord Real.compare string_ord o apply2 swap) end (* Ugly hack: may make innocent victims (collateral damage) *) @@ -2733,8 +2733,7 @@ fun strip_iff_etc (ATyQuant (_, _, phi)) = strip_iff_etc phi | strip_iff_etc (AQuant (_, _, phi)) = strip_iff_etc phi - | strip_iff_etc (AConn (AIff, [phi1, phi2])) = - pairself strip_up_to_predicator (phi1, phi2) + | strip_iff_etc (AConn (AIff, [phi1, phi2])) = apply2 strip_up_to_predicator (phi1, phi2) | strip_iff_etc _ = ([], []) val max_term_order_weight = 2147483647 @@ -2800,7 +2799,7 @@ in (* Sorting is not just for aesthetics: It specifies the precedence order for the term ordering (KBO or LPO), from smaller to larger values. *) - [] |> add_weights 1 (Graph.minimals graph) |> sort (int_ord o pairself snd) + [] |> add_weights 1 (Graph.minimals graph) |> sort (int_ord o apply2 snd) end end; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/ATP/atp_proof.ML Wed Nov 26 20:05:34 2014 +0100 @@ -243,7 +243,7 @@ (* Splits by the first possible of a list of delimiters. *) fun extract_tstplike_proof delims output = - (case pairself (find_first (fn s => String.isSubstring s output)) (ListPair.unzip delims) of + (case apply2 (find_first (fn s => String.isSubstring s output)) (ListPair.unzip delims) of (SOME begin_delim, SOME end_delim) => extract_delimited (begin_delim, end_delim) output | _ => "") @@ -269,9 +269,9 @@ val vampire_fact_prefix = "f" fun vampire_step_name_ord p = - let val q = pairself fst p in + let val q = apply2 fst p in (* The "unprefix" part is to cope with Vampire's output. *) - (case pairself (Int.fromString o perhaps (try (unprefix vampire_fact_prefix))) q of + (case apply2 (Int.fromString o perhaps (try (unprefix vampire_fact_prefix))) q of (SOME i, SOME j) => int_ord (i, j) | _ => raise Fail "not Vampire") end @@ -286,8 +286,8 @@ with "$" and possibly with "!" in them (for "z3_tptp"). *) val scan_general_id = $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode - || (Scan.repeat ($$ "$") -- Scan.many1 Symbol.is_letdig >> (op ^ o pairself implode)) - -- Scan.optional (Scan.repeat ($$ "!") -- Scan.many1 Symbol.is_letdig >> (op ^ o pairself implode)) "" + || (Scan.repeat ($$ "$") -- Scan.many1 Symbol.is_letdig >> (op ^ o apply2 implode)) + -- Scan.optional (Scan.repeat ($$ "!") -- Scan.many1 Symbol.is_letdig >> (op ^ o apply2 implode)) "" >> op ^ val skip_term = @@ -429,7 +429,7 @@ else K NONE) end | do_term_pair (ATerm ((s1, _), args1)) (ATerm ((s2, _), args2)) (SOME subst) = - (case pairself is_tptp_variable (s1, s2) of + (case apply2 is_tptp_variable (s1, s2) of (true, true) => (case AList.lookup (op =) subst s1 of SOME s2' => if s2' = s2 then SOME subst else NONE diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed Nov 26 20:05:34 2014 +0100 @@ -674,7 +674,7 @@ val (haves, have_nots) = HOLogic.disjuncts t |> List.partition (exists_subterm (curry (op =) (Var v))) - |> pairself (fn lits => fold (curry s_disj) lits @{term False}) + |> apply2 (fn lits => fold (curry s_disj) lits @{term False}) in s_disj (HOLogic.all_const T $ Abs (s, T, unskolem (safe_abstract_over (Var v, kill_skolem_arg haves))), diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/ATP/atp_proof_redirect.ML --- a/src/HOL/Tools/ATP/atp_proof_redirect.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML Wed Nov 26 20:05:34 2014 +0100 @@ -68,7 +68,7 @@ val atom_eq = is_equal o Atom.ord val clause_ord = dict_ord Atom.ord -fun direct_sequent_ord seqp = prod_ord clause_ord clause_ord (pairself snd seqp) +fun direct_sequent_ord seqp = prod_ord clause_ord clause_ord (apply2 snd seqp) fun direct_sequent_eq seqp = is_equal (direct_sequent_ord seqp) fun make_refute_graph bot infers = diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/ATP/atp_satallax.ML --- a/src/HOL/Tools/ATP/atp_satallax.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/ATP/atp_satallax.ML Wed Nov 26 20:05:34 2014 +0100 @@ -426,7 +426,7 @@ | NONE => tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *) |> parse_proof local_prover problem - |> local_prover = vampireN ? perhaps (try (sort (vampire_step_name_ord o pairself #1))) + |> local_prover = vampireN ? perhaps (try (sort (vampire_step_name_ord o apply2 #1))) |> local_prover = zipperpositionN ? rev) end; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/BNF/bnf_comp.ML --- a/src/HOL/Tools/BNF/bnf_comp.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_comp.ML Wed Nov 26 20:05:34 2014 +0100 @@ -655,7 +655,7 @@ end; fun default_comp_sort Ass = - Library.sort (Term_Ord.typ_ord o pairself TFree) (fold (fold (insert (op =))) Ass []); + Library.sort (Term_Ord.typ_ord o apply2 TFree) (fold (fold (insert (op =))) Ass []); fun raw_compose_bnf const_policy qualify flatten_tyargs outer inners oDs Dss tfreess accum = let @@ -914,7 +914,7 @@ val lives = lives_of_bnf bnf; val tvars' = Term.add_tvarsT T' []; val Ds_As = - pairself (map (Term.typ_subst_TVars (map fst tvars' ~~ map TFree tfrees))) + apply2 (map (Term.typ_subst_TVars (map fst tvars' ~~ map TFree tfrees))) (deads, lives); in ((bnf, Ds_As), accum) end else diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/BNF/bnf_def.ML --- a/src/HOL/Tools/BNF/bnf_def.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_def.ML Wed Nov 26 20:05:34 2014 +0100 @@ -782,7 +782,7 @@ end; fun maybe_restore lthy_old lthy = - lthy |> not (Theory.eq_thy (pairself Proof_Context.theory_of (lthy_old, lthy))) + lthy |> not (Theory.eq_thy (apply2 Proof_Context.theory_of (lthy_old, lthy))) ? Local_Theory.restore; val map_bind_def = diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Nov 26 20:05:34 2014 +0100 @@ -2167,7 +2167,7 @@ val sel_bTs = flat sel_bindingss ~~ flat sel_Tss |> filter_out (Binding.is_empty o fst) - |> distinct (Binding.eq_name o pairself fst); + |> distinct (Binding.eq_name o apply2 fst); val sel_default_lthy = fake_local_theory_for_sel_defaults sel_bTs lthy; val sel_default_eqs = map (prepare_term sel_default_lthy) raw_sel_default_eqs; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/BNF/bnf_fp_n2m.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Wed Nov 26 20:05:34 2014 +0100 @@ -74,7 +74,7 @@ val nesting_bnfss = map (fn sugar => #fp_nesting_bnfs sugar @ #live_nesting_bnfs sugar) fp_sugars; val fp_or_nesting_bnfss = fp_bnfs :: nesting_bnfss; - val fp_or_nesting_bnfs = distinct (op = o pairself T_of_bnf) (flat fp_or_nesting_bnfss); + val fp_or_nesting_bnfs = distinct (op = o apply2 T_of_bnf) (flat fp_or_nesting_bnfss); val fp_absTs = map #absT fp_absT_infos; val fp_repTs = map #repT fp_absT_infos; @@ -139,7 +139,7 @@ val rels = let fun find_rel T As Bs = fp_or_nesting_bnfss - |> map (filter_out (curry (op = o pairself name_of_bnf) BNF_Comp.DEADID_bnf)) + |> map (filter_out (curry (op = o apply2 name_of_bnf) BNF_Comp.DEADID_bnf)) |> get_first (find_first (fn bnf => Type.could_unify (T_of_bnf bnf, T))) |> Option.map (fn bnf => let val live = live_of_bnf bnf; @@ -191,7 +191,7 @@ case_fp fp (snd o Term.dest_comb) (snd o Term.dest_comb o fst o Term.dest_comb); val raw_phis = map (extract o HOLogic.dest_Trueprop o Thm.concl_of) rel_xtor_co_inducts; val thetas = AList.group (op =) - (mutual_cliques ~~ map (pairself (certify lthy)) (raw_phis ~~ pre_phis)); + (mutual_cliques ~~ map (apply2 (certify lthy)) (raw_phis ~~ pre_phis)); in map2 (Drule.cterm_instantiate o the o AList.lookup (op =) thetas) mutual_cliques rel_xtor_co_inducts @@ -286,7 +286,7 @@ val fold_pre_deads_only_Ts = map (typ_subst_nonatomic_sorted (map (rpair dummyT) - (As @ sort (int_ord o pairself Term.size_of_typ) fpTs))) fold_preTs'; + (As @ sort (int_ord o apply2 Term.size_of_typ) fpTs))) fold_preTs'; val (mutual_clique, TUs) = map_split dest_co_algT (binder_fun_types (foldT_of_recT (fastype_of approx_rec))) @@ -439,7 +439,7 @@ @{thms fst_convol map_prod_o_convol convol_o fst_comp_map_prod} @{thms case_sum_o_inj(1) case_sum_o_map_sum o_case_sum map_sum_o_inj(1)}; - val eq_thm_prop_untyped = Term.aconv_untyped o pairself Thm.full_prop_of; + val eq_thm_prop_untyped = Term.aconv_untyped o apply2 Thm.full_prop_of; val map_thms = no_refl (maps (fn bnf => let val map_comp0 = map_comp0_of_bnf bnf RS sym diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Wed Nov 26 20:05:34 2014 +0100 @@ -390,7 +390,7 @@ (if Ts1 = Ts2 andalso length Ts1 = 1 then "itself" else qsotys Ts2)); val sorted_actual_Ts = - sort (prod_ord int_ord Term_Ord.typ_ord o pairself (`Term.size_of_typ)) actual_Ts; + sort (prod_ord int_ord Term_Ord.typ_ord o apply2 (`Term.size_of_typ)) actual_Ts; fun the_ctrs_of (Type (s, Ts)) = map (mk_ctr Ts) (#ctrs (the (ctr_sugar_of lthy s))); diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Wed Nov 26 20:05:34 2014 +0100 @@ -578,7 +578,7 @@ val n = Thm.nprems_of coind; val m = Thm.nprems_of (hd rel_monos) - n; fun mk_inst phi = (phi, mk_union (phi, HOLogic.eq_const (fst (dest_pred2T (fastype_of phi))))) - |> pairself (certify ctxt); + |> apply2 (certify ctxt); val insts = Term.add_vars (Thm.prop_of coind) [] |> rev |> take n |> map (mk_inst o Var); fun mk_unfold rel_eq rel_mono = let diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Wed Nov 26 20:05:34 2014 +0100 @@ -128,7 +128,7 @@ fun unexpected_corec_call ctxt t = error ("Unexpected corecursive call: " ^ quote (Syntax.string_of_term ctxt t)); -fun sort_list_duplicates xs = map snd (sort (int_ord o pairself fst) xs); +fun sort_list_duplicates xs = map snd (sort (int_ord o apply2 fst) xs); val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default @{const True}; val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default @{const False}; @@ -415,7 +415,7 @@ val coinduct_attrs_pair = (case gfp_sugar_thms of SOME ((_, attrs_pair), _, _, _, _) => attrs_pair | NONE => ([], [])); - val perm_fp_sugars = sort (int_ord o pairself #fp_res_index) fp_sugars; + val perm_fp_sugars = sort (int_ord o apply2 #fp_res_index) fp_sugars; val indices = map #fp_res_index fp_sugars; val perm_indices = map #fp_res_index perm_fp_sugars; @@ -998,7 +998,7 @@ val callssss = map_filter (try (fn Sel x => x)) eqns_data - |> partition_eq (op = o pairself #fun_name) + |> partition_eq (op = o apply2 #fun_name) |> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names |> map (flat o snd) |> map2 (fold o find_corec_calls lthy has_call) basic_ctr_specss @@ -1012,21 +1012,24 @@ val ctr_specss = map #ctr_specs corec_specs; val disc_eqnss' = map_filter (try (fn Disc x => x)) eqns_data - |> partition_eq (op = o pairself #fun_name) + |> partition_eq (op = o apply2 #fun_name) |> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names - |> map (sort (op < o pairself #ctr_no |> make_ord) o flat o snd); + |> map (sort (op < o apply2 #ctr_no |> make_ord) o flat o snd); val _ = disc_eqnss' |> map (fn x => - let val d = duplicates (op = o pairself #ctr_no) x in null d orelse - (if forall (is_some o #ctr_rhs_opt) x then - primcorec_error_eqns "multiple equations for constructor(s)" - (maps (fn t => filter (curry (op =) (#ctr_no t) o #ctr_no) x) d - |> map (the o #ctr_rhs_opt)) else - primcorec_error_eqns "excess discriminator formula in definition" - (maps (fn t => filter (curry (op =) (#ctr_no t) o #ctr_no) x) d |> map #user_eqn)) end); + let val d = duplicates (op = o apply2 #ctr_no) x in + null d orelse + (if forall (is_some o #ctr_rhs_opt) x then + primcorec_error_eqns "multiple equations for constructor(s)" + (maps (fn t => filter (curry (op =) (#ctr_no t) o #ctr_no) x) d + |> map (the o #ctr_rhs_opt)) + else + primcorec_error_eqns "excess discriminator formula in definition" + (maps (fn t => filter (curry (op =) (#ctr_no t) o #ctr_no) x) d |> map #user_eqn)) + end); val sel_eqnss = map_filter (try (fn Sel x => x)) eqns_data - |> partition_eq (op = o pairself #fun_name) + |> partition_eq (op = o apply2 #fun_name) |> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names |> map (flat o snd); @@ -1316,7 +1319,7 @@ let val ms = map (Logic.count_prems o prop_of) ctr_thms; val (raw_goal, goal) = (raw_rhs, rhs) - |> pairself (curry mk_Trueprop_eq (applied_fun_of fun_name fun_T fun_args) + |> apply2 (curry mk_Trueprop_eq (applied_fun_of fun_name fun_T fun_args) #> curry Logic.list_all (map dest_Free fun_args)); val (distincts, discIs, _, split_sels, split_sel_asms) = case_thms_of_term lthy raw_rhs; @@ -1372,7 +1375,7 @@ val ctr_alists = @{map 6} (fn disc_alist => maps oooo prove_ctr disc_alist) disc_alists (map (map snd) sel_alists) corec_specs disc_eqnss sel_eqnss ctr_specss; val ctr_thmss0 = map (map snd) ctr_alists; - val ctr_thmss = map (map (snd o snd) o sort (int_ord o pairself fst)) ctr_alists; + val ctr_thmss = map (map (snd o snd) o sort (int_ord o apply2 fst)) ctr_alists; val code_thmss = @{map 6} prove_code exhaustives disc_eqnss sel_eqnss nchotomy_thmss ctr_thmss0 ctr_specss; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/BNF/bnf_lfp_compat.ML --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Wed Nov 26 20:05:34 2014 +0100 @@ -402,13 +402,13 @@ val k = find_index (fn (_, (_, dTs, _)) => not (forall is_DtTFree dTs)) descr; val protoTs as (dataTs, _) = chop k descr - |> (pairself o map) + |> (apply2 o map) (fn (_, (T_name, Ds, _)) => (T_name, map (Old_Datatype_Aux.typ_of_dtyp descr) Ds)); val T_names = map fst dataTs; val _ = eq_set (op =) (T_names, T_names0) orelse not_mutually_recursive T_names0 - val (Ts, Us) = (pairself o map) Type protoTs; + val (Ts, Us) = apply2 (map Type) protoTs; val names = map Long_Name.base_name T_names; val (auxnames, _) = Name.make_context names diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Wed Nov 26 20:05:34 2014 +0100 @@ -182,7 +182,7 @@ common_induct, induct_attrs, n2m, lthy) = basic_lfp_sugars_of bs arg_Ts callers callssss0 lthy0; - val perm_basic_lfp_sugars = sort (int_ord o pairself #fp_res_index) basic_lfp_sugars; + val perm_basic_lfp_sugars = sort (int_ord o apply2 #fp_res_index) basic_lfp_sugars; val indices = map #fp_res_index basic_lfp_sugars; val perm_indices = map #fp_res_index perm_basic_lfp_sugars; @@ -421,10 +421,10 @@ val recs = take n_funs rec_specs |> map #recx; val rec_args = ctr_spec_eqn_data_list - |> sort (op < o pairself (#offset o fst) |> make_ord) + |> sort (op < o apply2 (#offset o fst) |> make_ord) |> map (uncurry (build_rec_arg ctxt funs_data has_call) o apsnd (try the_single)); val ctr_poss = map (fn x => - if length (distinct (op = o pairself (length o #left_args)) x) <> 1 then + if length (distinct (op = o apply2 (length o #left_args)) x) <> 1 then raise PRIMREC ("inconstant constructor pattern position for function " ^ quote (#fun_name (hd x)), []) else @@ -480,7 +480,7 @@ val fun_names = map Binding.name_of bs; val eqns_data = map (dissect_eqn lthy0 fun_names) specs; val funs_data = eqns_data - |> partition_eq (op = o pairself #fun_name) + |> partition_eq (op = o apply2 #fun_name) |> finds (fn (x, y) => x = #fun_name (hd y)) fun_names |> fst |> map (fn (x, y) => the_single y handle List.Empty => raise PRIMREC ("missing equations for function " ^ quote x, [])); @@ -490,7 +490,7 @@ val arg_Ts = map (#rec_type o hd) funs_data; val res_Ts = map (#res_type o hd) funs_data; val callssss = funs_data - |> map (partition_eq (op = o pairself #ctr)) + |> map (partition_eq (op = o apply2 #ctr)) |> map (maps (map_filter (find_rec_calls has_call))); fun is_only_old_datatype (Type (s, _)) = @@ -519,7 +519,7 @@ : rec_spec) (fun_data : eqn_data list) = let val js = - find_indices (op = o pairself (fn {fun_name, ctr, ...} => (fun_name, ctr))) + find_indices (op = o apply2 (fn {fun_name, ctr, ...} => (fun_name, ctr))) fun_data eqns_data; val def_thms = map (snd o snd) def_thms'; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/BNF/bnf_lfp_size.ML --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Wed Nov 26 20:05:34 2014 +0100 @@ -362,7 +362,7 @@ |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => Data.map (fold2 (fn T_name => fn Const (size_name, _) => Symtab.update (T_name, (size_name, - pairself (map (Morphism.thm (phi0 $> phi))) (size_simps, flat size_gen_o_map_thmss)))) + apply2 (map (Morphism.thm (phi0 $> phi))) (size_simps, flat size_gen_o_map_thmss)))) T_names size_consts)) end | generate_datatype_size _ lthy = lthy; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/BNF/bnf_tactics.ML --- a/src/HOL/Tools/BNF/bnf_tactics.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_tactics.ML Wed Nov 26 20:05:34 2014 +0100 @@ -51,7 +51,7 @@ (*transforms f (g x) = h (k x) into f o g = h o k using first order matches for f, g, h, and k*) fun mk_pointfree ctxt thm = thm |> Thm.prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq - |> pairself (dest_comb #> apsnd (dest_comb #> fst) #> HOLogic.mk_comp) + |> apply2 (dest_comb #> apsnd (dest_comb #> fst) #> HOLogic.mk_comp) |> mk_Trueprop_eq |> (fn goal => Goal.prove_sorry ctxt [] [] goal (K (rtac @{thm ext} 1 THEN diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Ctr_Sugar/case_translation.ML --- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML Wed Nov 26 20:05:34 2014 +0100 @@ -283,7 +283,7 @@ else raise CASE_ERROR ("Wrong number of arguments for constructor " ^ quote name, i) else ((in_group, row :: not_in_group), names) | _ => raise CASE_ERROR ("Not a constructor pattern", i))) - rows (([], []), replicate k "") |>> pairself rev + rows (([], []), replicate k "") |>> apply2 rev end; @@ -506,7 +506,7 @@ (Const (s, map fastype_of xs ---> fastype_of x), p, is_dependent k t) end) (constructors ~~ fs); val cases' = - sort (int_ord o swap o pairself (length o snd)) + sort (int_ord o swap o apply2 (length o snd)) (fold_rev count_cases cases []); val R = fastype_of t; val dummy = diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Wed Nov 26 20:05:34 2014 +0100 @@ -549,7 +549,7 @@ val all_proto_sels = flat (@{map 3} (fn k => fn xs => map (pair k o pair xs)) ks xss xss); val sel_infos = AList.group (op =) (sel_binding_index ~~ all_proto_sels) - |> sort (int_ord o pairself fst) + |> sort (int_ord o apply2 fst) |> map snd |> curry (op ~~) uniq_sel_bindings; val sel_bindings = map fst sel_infos; @@ -666,7 +666,7 @@ let val ((inject_thms, inject_thmss), half_distinct_thmss) = chop n thmss |>> `flat; - val rho_As = map (pairself (certifyT lthy)) (map Logic.varifyT_global As ~~ As); + val rho_As = map (apply2 (certifyT lthy)) (map Logic.varifyT_global As ~~ As); fun inst_thm t thm = Drule.instantiate' [] [SOME (certify lthy t)] @@ -717,7 +717,7 @@ in (Goal.prove_sorry lthy [] [] goal (fn _ => mk_case_cong_tac lthy uexhaust_thm case_thms), Goal.prove_sorry lthy [] [] weak_goal (K (etac arg_cong 1))) - |> pairself (singleton (Proof_Context.export names_lthy lthy) #> + |> apply2 (singleton (Proof_Context.export names_lthy lthy) #> Thm.close_derivation) end; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Function/function_common.ML --- a/src/HOL/Tools/Function/function_common.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Function/function_common.ML Wed Nov 26 20:05:34 2014 +0100 @@ -177,7 +177,7 @@ structure FunctionData = Generic_Data ( type T = (term * info) Item_Net.T; - val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst); + val empty : T = Item_Net.init (op aconv o apply2 fst) (single o fst); val extend = I; fun merge tabs : T = Item_Net.merge tabs; ) diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Function/induction_schema.ML --- a/src/HOL/Tools/Function/induction_schema.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Function/induction_schema.ML Wed Nov 26 20:05:34 2014 +0100 @@ -339,7 +339,7 @@ |> (curry op COMP) wf_thm |> (curry op COMP) istep - val steps_sorted = map snd (sort (int_ord o pairself fst) steps) + val steps_sorted = map snd (sort (int_ord o apply2 fst) steps) in (steps_sorted, induct_rule) end @@ -356,8 +356,7 @@ val x = Free (xn, ST) val cert = cterm_of (Proof_Context.theory_of ctxt) - val ineqss = mk_ineqs R scheme - |> map (map (pairself (Thm.assume o cert))) + val ineqss = mk_ineqs R scheme |> map (map (apply2 (Thm.assume o cert))) val complete = map_range (mk_completeness ctxt scheme #> cert #> Thm.assume) (length branches) val wf_thm = mk_wf R scheme |> cert |> Thm.assume diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Function/pat_completeness.ML --- a/src/HOL/Tools/Function/pat_completeness.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Function/pat_completeness.ML Wed Nov 26 20:05:34 2014 +0100 @@ -26,8 +26,7 @@ fun inst_case_thm thy x P thm = let val [Pv, xv] = Term.add_vars (prop_of thm) [] in - thm |> cterm_instantiate (map (pairself (cterm_of thy)) - [(Var xv, x), (Var Pv, P)]) + thm |> cterm_instantiate (map (apply2 (cterm_of thy)) [(Var xv, x), (Var Pv, P)]) end fun invent_vars constr i = diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Lifting/lifting_bnf.ML --- a/src/HOL/Tools/Lifting/lifting_bnf.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Lifting/lifting_bnf.ML Wed Nov 26 20:05:34 2014 +0100 @@ -23,7 +23,7 @@ fun get_lhs thm = thm |> concl_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst val vars = get_lhs rel_Grp |> strip_comb |> snd |> map_filter (try (strip_comb #> snd #> hd)) val UNIVs = map (fn var => HOLogic.mk_UNIV (var |> dest_Var |> snd |> dest_Type |> snd |> hd)) vars - val inst = map2 (curry(pairself (certify ctxt))) vars UNIVs + val inst = map2 (curry (apply2 (certify ctxt))) vars UNIVs val rel_Grp_UNIV_sym = rel_Grp |> Drule.instantiate_normalize ([], inst) |> Local_Defs.unfold ctxt @{thms subset_UNIV[THEN eqTrueI] UNIV_def[symmetric] simp_thms(21)} |> (fn thm => thm RS sym) diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Lifting/lifting_def.ML --- a/src/HOL/Tools/Lifting/lifting_def.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Lifting/lifting_def.ML Wed Nov 26 20:05:34 2014 +0100 @@ -99,7 +99,7 @@ end; val subst = fold make_subst free_vars []; - val csubst = map (pairself (cterm_of thy)) subst; + val csubst = map (apply2 (cterm_of thy)) subst; val inst_thm = Drule.cterm_instantiate csubst thm; in Conv.fconv_rule diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Lifting/lifting_info.ML --- a/src/HOL/Tools/Lifting/lifting_info.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Lifting/lifting_info.ML Wed Nov 26 20:05:34 2014 +0100 @@ -306,15 +306,16 @@ val dest_less_eq = HOLogic.dest_bin @{const_name "less_eq"} dummyT val prems_pairs = map (dest_less_eq o HOLogic.dest_Trueprop) (prems_of rule) val equal_prems = filter op= prems_pairs - val _ = if null equal_prems then () + val _ = + if null equal_prems then () else error "The rule contains reflexive assumptions." val concl_pairs = rule |> concl_of |> HOLogic.dest_Trueprop |> dest_less_eq - |> pairself (snd o strip_comb) - |> op~~ - |> filter_out op= + |> apply2 (snd o strip_comb) + |> op ~~ + |> filter_out op = val _ = if has_duplicates op= concl_pairs then error "The rule contains duplicated variables in the conlusion." else () @@ -323,7 +324,7 @@ if member op= concl_pairs prem_pair then HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm POS_def})) else if member op= concl_pairs (swap prem_pair) - then HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm NEG_def})) + then HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm NEG_def})) else error "The rule contains a non-relevant assumption." fun rewrite_prems [] = Conv.all_conv diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Meson/meson.ML --- a/src/HOL/Tools/Meson/meson.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Meson/meson.ML Wed Nov 26 20:05:34 2014 +0100 @@ -109,7 +109,7 @@ val tenv = Pattern.first_order_match thy (tmB, tmA) (Vartab.empty, Vartab.empty) |> snd - val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv) + val ct_pairs = map (apply2 (cterm_of thy) o term_pair_of) (Vartab.dest tenv) in thA RS (cterm_instantiate ct_pairs thB) end) () of SOME th => th | NONE => raise THM ("first_order_resolve", 0, [thA, thB])) @@ -594,7 +594,7 @@ let fun pat t u = let - val ((head1, args1), (head2, args2)) = (t, u) |> pairself strip_comb + val ((head1, args1), (head2, args2)) = (t, u) |> apply2 strip_comb in if head1 = head2 then let val pats = map2 pat args1 args2 in @@ -631,7 +631,7 @@ $ (t as _ $ _) $ (u as _ $ _))) => (case get_F_pattern T t u of SOME p => - let val inst = [pairself (cterm_of thy) (F_ext_cong_neq, p)] in + let val inst = [apply2 (cterm_of thy) (F_ext_cong_neq, p)] in th RS cterm_instantiate inst ext_cong_neq end | NONE => th) diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Meson/meson_clausify.ML --- a/src/HOL/Tools/Meson/meson_clausify.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Wed Nov 26 20:05:34 2014 +0100 @@ -375,7 +375,7 @@ th ctxt ctxt val (cnf_ths, ctxt) = clausify nnf_th fun intr_imp ct th = - Thm.instantiate ([], map (pairself (cterm_of thy)) + Thm.instantiate ([], map (apply2 (cterm_of thy)) [(Var (("i", 0), @{typ nat}), HOLogic.mk_nat ax_no)]) (zero_var_indexes @{thm skolem_COMBK_D}) diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Metis/metis_generate.ML --- a/src/HOL/Tools/Metis/metis_generate.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Metis/metis_generate.ML Wed Nov 26 20:05:34 2014 +0100 @@ -207,7 +207,7 @@ |> map (pair 0) |> Monomorph.monomorph atp_schematic_consts_of ctxt |> chop (length conj_clauses) - |> pairself (maps (map (zero_var_indexes o snd))) + |> apply2 (maps (map (zero_var_indexes o snd))) val num_conjs = length conj_clauses (* Pretend every clause is a "simp" rule, to guide the term ordering. *) val clauses = diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Nov 26 20:05:34 2014 +0100 @@ -175,7 +175,7 @@ let val tvs = Term.add_tvars (Thm.full_prop_of th) [] val thy = Thm.theory_of_thm th - fun inc_tvar ((a, i), s) = pairself (ctyp_of thy) (TVar ((a, i), s), TVar ((a, i + inc), s)) + fun inc_tvar ((a, i), s) = apply2 (ctyp_of thy) (TVar ((a, i), s), TVar ((a, i + inc), s)) in Thm.instantiate (map inc_tvar tvs, []) th end @@ -213,7 +213,7 @@ |> rpair (Envir.empty ~1) |-> fold (Pattern.unify (Context.Proof ctxt)) |> Envir.type_env |> Vartab.dest - |> map (fn (x, (S, T)) => pairself (ctyp_of thy) (TVar (x, S), T)) + |> map (fn (x, (S, T)) => apply2 (ctyp_of thy) (TVar (x, S), T)) in (* The unifier, which is invoked from "Thm.bicompose", will sometimes refuse to unify "?a::?'a" with "?a::?'b" or "?a::nat" and throw a "TERM" exception (with "add_ffpair" as @@ -221,7 +221,7 @@ again. We could do this the first time around but this error occurs seldom and we don't want to break existing proofs in subtle ways or slow them down. *) if null ps then raise TERM z - else res (pairself (Drule.instantiate_normalize (ps, [])) (tha, thb)) + else res (apply2 (Drule.instantiate_normalize (ps, [])) (tha, thb)) end end @@ -270,7 +270,7 @@ fun resolve_inference ctxt type_enc concealed sym_tab th_pairs atom th1 th2 = let - val (i_th1, i_th2) = pairself (lookth th_pairs) (th1, th2) + val (i_th1, i_th2) = apply2 (lookth th_pairs) (th1, th2) val _ = trace_msg ctxt (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1 ^ "\n\ \ isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2) @@ -374,7 +374,7 @@ val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill-typed but gives right max*) val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em) val _ = trace_msg ctxt (fn () => "subst' " ^ Display.string_of_thm ctxt subst') - val eq_terms = map (pairself (cterm_of thy)) + val eq_terms = map (apply2 (cterm_of thy)) (ListPair.zip (Misc_Legacy.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm])) in cterm_instantiate eq_terms subst' @@ -522,7 +522,7 @@ | _ => I) val t_inst = - [] |> try (unify_terms (prem, concl) #> map (pairself (cterm_of thy))) + [] |> try (unify_terms (prem, concl) #> map (apply2 (cterm_of thy))) |> the_default [] (* FIXME *) in cterm_instantiate t_inst th @@ -574,8 +574,8 @@ Envir.Envir {maxidx = Vartab.fold (Integer.max o snd o fst) tyenv 0, tenv = Vartab.empty, tyenv = tyenv} val ty_inst = - Vartab.fold (fn (x, (S, T)) => cons (pairself (ctyp_of thy) (TVar (x, S), T))) tyenv [] - val t_inst = [pairself (cterm_of thy o Envir.norm_term env) (Var var, t')] + Vartab.fold (fn (x, (S, T)) => cons (apply2 (ctyp_of thy) (TVar (x, S), T))) tyenv [] + val t_inst = [apply2 (cterm_of thy o Envir.norm_term env) (Var var, t')] in Drule.instantiate_normalize (ty_inst, t_inst) th end @@ -617,7 +617,7 @@ fun cluster_key ((ax_no, (cluster_no, index_no)), skolem) = (ax_no, (cluster_no, (skolem, index_no))) fun cluster_ord p = - prod_ord int_ord (prod_ord int_ord (prod_ord bool_ord int_ord)) (pairself cluster_key p) + prod_ord int_ord (prod_ord int_ord (prod_ord bool_ord int_ord)) (apply2 cluster_key p) val tysubst_ord = list_ord (prod_ord Term_Ord.fast_indexname_ord (prod_ord Term_Ord.sort_ord Term_Ord.typ_ord)) @@ -630,7 +630,7 @@ Graph(type key = int * int val ord = prod_ord int_ord int_ord) fun shuffle_key (((axiom_no, (_, index_no)), _), _) = (axiom_no, index_no) -fun shuffle_ord p = prod_ord int_ord int_ord (pairself shuffle_key p) +fun shuffle_ord p = prod_ord int_ord int_ord (apply2 shuffle_key p) (* Attempts to derive the theorem "False" from a theorem of the form "P1 ==> ... ==> Pn ==> False", where the "Pi"s are to be discharged using the @@ -651,10 +651,9 @@ tenv |> Vartab.dest |> filter (Meson_Clausify.is_zapped_var_name o fst o fst) |> sort (cluster_ord - o pairself (Meson_Clausify.cluster_of_zapped_var_name + o apply2 (Meson_Clausify.cluster_of_zapped_var_name o fst o fst)) - |> map (Meson.term_pair_of - #> pairself (Envir.subst_term_types tyenv)) + |> map (Meson.term_pair_of #> apply2 (Envir.subst_term_types tyenv)) val tysubst = tyenv |> Vartab.dest in (tysubst, tsubst) end @@ -686,7 +685,7 @@ val prems = Logic.strip_imp_prems (prop_of prems_imp_false) val substs = prems |> map2 subst_info_of_prem (1 upto length prems) - |> sort (int_ord o pairself fst) + |> sort (int_ord o apply2 fst) val depss = maps (map_filter deps_of_term_subst o snd o snd o snd) substs val clusters = maps (op ::) depss val ordered_clusters = @@ -725,7 +724,7 @@ "ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^ "; tysubst: " ^ @{make_string} tysubst ^ "; tsubst: {" ^ commas (map ((fn (s, t) => s ^ " |-> " ^ t) - o pairself (Syntax.string_of_term ctxt)) tsubst) ^ "}" + o apply2 (Syntax.string_of_term ctxt)) tsubst) ^ "}" val _ = tracing ("ORDERED CLUSTERS: " ^ @{make_string} ordered_clusters) val _ = tracing ("AXIOM COUNTS: " ^ @{make_string} ax_counts) val _ = tracing ("OUTER PARAMS: " ^ @{make_string} outer_param_names) diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Metis/metis_tactic.ML --- a/src/HOL/Tools/Metis/metis_tactic.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Metis/metis_tactic.ML Wed Nov 26 20:05:34 2014 +0100 @@ -33,7 +33,7 @@ (* Designed to work also with monomorphic instances of polymorphic theorems. *) fun have_common_thm ths1 ths2 = - exists (member (Term.aconv_untyped o pairself prop_of) ths1) (map Meson.make_meta_clause ths2) + exists (member (Term.aconv_untyped o apply2 prop_of) ths1) (map Meson.make_meta_clause ths2) (*Determining which axiom clauses are actually used*) fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th) @@ -126,7 +126,7 @@ fun weight (m, _) = AList.lookup (op =) ord_info (Metis_Name.toString m) |> the_default 1 fun precedence p = - (case int_ord (pairself weight p) of + (case int_ord (apply2 weight p) of EQUAL => #precedence Metis_KnuthBendixOrder.default p | ord => ord) in {weight = weight, precedence = precedence} end diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Nitpick/nitpick_commands.ML --- a/src/HOL/Tools/Nitpick/nitpick_commands.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML Wed Nov 26 20:05:34 2014 +0100 @@ -187,7 +187,7 @@ | ["", s2] => ("-" ^ s2, "-" ^ s2) | [s1, s2] => (s1, s2) | _ => raise Option.Option) - |> pairself (maxed_int_from_string min_int) + |> apply2 (maxed_int_from_string min_int) in if k1 <= k2 then k1 upto k2 else k1 downto k2 end handle Option.Option => error ("Parameter " ^ quote name ^ diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Nov 26 20:05:34 2014 +0100 @@ -324,7 +324,7 @@ val strip_first_name_sep = Substring.full #> Substring.position name_sep ##> Substring.triml 1 - #> pairself Substring.string + #> apply2 Substring.string fun original_name s = if String.isPrefix nitpick_prefix s then @@ -460,7 +460,7 @@ (Sign.typ_match thy (T2, T1) Vartab.empty; true) handle Type.TYPE_MATCH => false -fun type_match thy = strict_type_match thy o pairself unarize_unbox_etc_type +fun type_match thy = strict_type_match thy o apply2 unarize_unbox_etc_type fun const_match thy ((s1, T1), (s2, T2)) = s1 = s2 andalso type_match thy (T1, T2) @@ -1329,7 +1329,7 @@ | is_ground_term _ = false fun special_bounds ts = - fold Term.add_vars ts [] |> sort (Term_Ord.fast_indexname_ord o pairself fst) + fold Term.add_vars ts [] |> sort (Term_Ord.fast_indexname_ord o apply2 fst) fun is_funky_typedef_name ctxt s = member (op =) [@{type_name unit}, @{type_name prod}, @{type_name set}, @@ -1350,7 +1350,7 @@ Theory.nodes_of thy |> maps Thm.axioms_of |> map (apsnd (subst_atomic subst o prop_of)) - |> sort (fast_string_ord o pairself fst) + |> sort (fast_string_ord o apply2 fst) |> Ord_List.inter (fast_string_ord o apsnd fst) def_names |> map snd end @@ -1607,7 +1607,7 @@ discriminate_value hol_ctxt x (Bound 0))) |> AList.group (op aconv) |> map (apsnd (List.foldl s_disj @{const False})) - |> sort (int_ord o pairself (size_of_term o snd)) + |> sort (int_ord o apply2 (size_of_term o snd)) |> rev in if res_T = bool_T then @@ -1727,7 +1727,7 @@ else do_const depth Ts t x [t1, t2, t3] | Const (@{const_name Let}, _) $ t1 $ t2 => - s_betapply Ts (pairself (do_term depth Ts) (t2, t1)) + s_betapply Ts (apply2 (do_term depth Ts) (t2, t1)) | Const x => do_const depth Ts t x [] | t1 $ t2 => (case strip_comb t of @@ -1979,7 +1979,7 @@ in typedef_info ctxt (fst (dest_Type abs_T)) |> the |> pairf #Abs_inverse #Rep_inverse - |> pairself (specialize_type thy x o prop_of o the) + |> apply2 (specialize_type thy x o prop_of o the) ||> single |> op :: end @@ -2089,7 +2089,7 @@ fun wf_constraint_for rel side concl main = let val core = HOLogic.mk_mem (HOLogic.mk_prod - (pairself tuple_for_args (main, concl)), Var rel) + (apply2 tuple_for_args (main, concl)), Var rel) val t = List.foldl HOLogic.mk_imp core side val vars = filter_out (curry (op =) rel) (Term.add_vars t []) in @@ -2182,7 +2182,7 @@ end fun num_occs_of_bound_in_term j (t1 $ t2) = - op + (pairself (num_occs_of_bound_in_term j) (t1, t2)) + op + (apply2 (num_occs_of_bound_in_term j) (t1, t2)) | num_occs_of_bound_in_term j (Abs (_, _, t')) = num_occs_of_bound_in_term (j + 1) t' | num_occs_of_bound_in_term j (Bound j') = if j' = j then 1 else 0 @@ -2397,7 +2397,7 @@ filter_out (fn (S', _) => Sign.subsort thy (S, S')) #> cons (S, s)) val tfrees = [] |> fold Term.add_tfrees ts - |> sort (string_ord o pairself fst) + |> sort (string_ord o apply2 fst) in [] |> fold add tfrees |> rev end fun merge_type_vars_in_term thy merge_type_vars table = diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Wed Nov 26 20:05:34 2014 +0100 @@ -201,12 +201,12 @@ fun tabulate_int_op2 debug univ_card (k, j0) f = tabulate_op2 debug univ_card (k, j0) j0 - (atom_for_int (k, 0) o f o pairself (int_for_atom (k, 0))) + (atom_for_int (k, 0) o f o apply2 (int_for_atom (k, 0))) fun tabulate_int_op2_2 debug univ_card (k, j0) f = tabulate_op2_2 debug univ_card (k, j0) j0 - (pairself (atom_for_int (k, 0)) o f - o pairself (int_for_atom (k, 0))) + (apply2 (atom_for_int (k, 0)) o f + o apply2 (int_for_atom (k, 0))) fun isa_div (m, n) = m div n handle General.Div => 0 fun isa_mod (m, n) = m mod n handle General.Div => m @@ -215,7 +215,7 @@ | isa_gcd (m, n) = isa_gcd (n, isa_mod (m, n)) fun isa_lcm (m, n) = isa_div (m * n, isa_gcd (m, n)) -val isa_zgcd = isa_gcd o pairself abs +val isa_zgcd = isa_gcd o apply2 abs fun isa_norm_frac (m, n) = if n < 0 then isa_norm_frac (~m, ~n) @@ -1058,7 +1058,7 @@ if card_of_rep R1 <> 1 then raise REP ("Nitpick_Kodkod.to_r (Converse)", [R]) else - pairself (Atom o pair 1 o offset_of_type ofs) (b_T, a_T) + apply2 (Atom o pair 1 o offset_of_type ofs) (b_T, a_T) | _ => raise REP ("Nitpick_Kodkod.to_r (Converse)", [R]) val body_R = body_rep R val a_arity = arity_of_rep a_R @@ -1163,7 +1163,7 @@ (fold kk_and (map_filter (fn (u, r) => if is_opt_rep (rep_of u) then SOME (kk_some r) else NONE) [(u1, r1), (u2, r2)]) KK.True) - (atom_from_formula kk bool_j0 (KK.LT (pairself + (atom_from_formula kk bool_j0 (KK.LT (apply2 (int_expr_from_atom kk (type_of u1)) (r1, r2)))) KK.None) (to_rep R1 u1) (to_rep R1 u2) @@ -1604,7 +1604,7 @@ (delta, (epsilon, (num_binder_types T, s))) val constr_ord = prod_ord int_ord (prod_ord int_ord (prod_ord int_ord string_ord)) - o pairself constr_quadruple + o apply2 constr_quadruple fun data_type_ord (({card = card1, self_rec = self_rec1, constrs = constr1, ...}, {card = card2, self_rec = self_rec2, constrs = constr2, ...}) diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Wed Nov 26 20:05:34 2014 +0100 @@ -107,7 +107,7 @@ Sign.declare_const_global ((@{binding nitpick_step}, @{typ "'a => 'a"}), Mixfix (step_mixfix (), [1000], 1000)) thy in - (pairself (pairself name_of) ((maybe_t, abs_t), (base_t, step_t)), + (apply2 (apply2 name_of) ((maybe_t, abs_t), (base_t, step_t)), Proof_Context.transfer thy ctxt) end @@ -158,7 +158,7 @@ | extract_real_number t = real (snd (HOLogic.dest_number t)) fun nice_term_ord (Abs (_, _, t1), Abs (_, _, t2)) = nice_term_ord (t1, t2) - | nice_term_ord tp = Real.compare (pairself extract_real_number tp) + | nice_term_ord tp = Real.compare (apply2 extract_real_number tp) handle TERM ("dest_number", _) => case tp of (t11 $ t12, t21 $ t22) => @@ -213,7 +213,7 @@ fun factor_out_types (T1 as Type (@{type_name prod}, [T11, T12])) (T2 as Type (@{type_name prod}, [T21, T22])) = - let val (n1, n2) = pairself num_factors_in_type (T11, T21) in + let val (n1, n2) = apply2 num_factors_in_type (T11, T21) in if n1 = n2 then let val ((T11', opt_T12'), (T21', opt_T22')) = factor_out_types T12 T22 @@ -259,13 +259,13 @@ (maybe_opt, (t1 :: ts1, t2 :: ts2)) end | aux t = raise TERM ("Nitpick_Model.dest_plain_fun", [t]) - in apsnd (pairself rev) o aux end + in apsnd (apply2 rev) o aux end fun break_in_two T T1 T2 t = let val ps = HOLogic.flat_tupleT_paths T val cut = length (HOLogic.strip_tupleT T1) - val (ps1, ps2) = pairself HOLogic.flat_tupleT_paths (T1, T2) + val (ps1, ps2) = apply2 HOLogic.flat_tupleT_paths (T1, T2) val (ts1, ts2) = t |> HOLogic.strip_ptuple ps |> chop cut in (HOLogic.mk_ptuple ps1 T1 ts1, HOLogic.mk_ptuple ps2 T2 ts2) end @@ -446,7 +446,7 @@ Type (@{type_name option}, [T2']) => let val (maybe_opt, ts_pair) = - dest_plain_fun t ||> pairself (map (polish_funs Ts)) + dest_plain_fun t ||> apply2 (map (polish_funs Ts)) in make_map maybe_opt T1 T2 T2' (rev (op ~~ ts_pair)) end | _ => raise SAME () else @@ -472,7 +472,7 @@ | t => t fun make_fun_or_set maybe_opt T T1 T2 T' ts1 ts2 = ts1 ~~ ts2 - |> sort (nice_term_ord o pairself fst) + |> sort (nice_term_ord o apply2 fst) |> (case T of Type (@{type_name set}, _) => sort_wrt (truth_const_sort_key o snd) @@ -703,7 +703,7 @@ fun intersect_formats _ [] = [] | intersect_formats [] _ = [] | intersect_formats ks1 ks2 = - let val ((ks1', k1), (ks2', k2)) = pairself split_last (ks1, ks2) in + let val ((ks1', k1), (ks2', k2)) = apply2 split_last (ks1, ks2) in intersect_formats (ks1' @ (if k1 > k2 then [k1 - k2] else [])) (ks2' @ (if k2 > k1 then [k2 - k1] else [])) @ [Int.min (k1, k2)] @@ -870,7 +870,7 @@ if exists_subtype (member (op =) coTs) T then let val ((head1, args1), (head2, args2)) = - pairself (strip_comb o unfold_outer_the_binders) (t1, t2) + apply2 (strip_comb o unfold_outer_the_binders) (t1, t2) val max_depth = max_depth - (if member (op =) coTs T then 1 else 0) in head1 = head2 andalso diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Nitpick/nitpick_mono.ML --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Wed Nov 26 20:05:34 2014 +0100 @@ -161,7 +161,7 @@ | repair_mtype cache seen (MFun (M1, aa, M2)) = MFun (repair_mtype cache seen M1, aa, repair_mtype cache seen M2) | repair_mtype cache seen (MPair Mp) = - MPair (pairself (repair_mtype cache seen) Mp) + MPair (apply2 (repair_mtype cache seen) Mp) | repair_mtype cache seen (MType (s, Ms)) = MType (s, maps (flatten_mtype o repair_mtype cache seen) Ms) | repair_mtype cache seen (MRec (z as (s, _))) = @@ -228,7 +228,7 @@ else case T of Type (@{type_name fun}, [T1, T2]) => MFun (fresh_mfun_for_fun_type mdata all_minus T1 T2) - | Type (@{type_name prod}, [T1, T2]) => MPair (pairself do_type (T1, T2)) + | Type (@{type_name prod}, [T1, T2]) => MPair (apply2 do_type (T1, T2)) | Type (@{type_name set}, [T']) => do_type (T' --> bool_T) | Type (z as (s, _)) => if could_exist_alpha_sub_mtype ctxt alpha_T T then @@ -320,7 +320,7 @@ fun aux MAlpha = MAlpha | aux (MFun (M1, aa, M2)) = MFun (aux M1, resolve_annotation_atom asgs aa, aux M2) - | aux (MPair Mp) = MPair (pairself aux Mp) + | aux (MPair Mp) = MPair (apply2 aux Mp) | aux (MType (s, Ms)) = MType (s, map aux Ms) | aux (MRec z) = MRec z in aux end @@ -506,8 +506,8 @@ fun prop_for_atom_equality (aa1, A a2) = prop_for_atom_assign (aa1, a2) | prop_for_atom_equality (A a1, aa2) = prop_for_atom_assign (aa2, a1) | prop_for_atom_equality (V x1, V x2) = - Prop_Logic.SAnd (prop_for_bool_var_equality (pairself fst_var (x1, x2)), - prop_for_bool_var_equality (pairself snd_var (x1, x2))) + Prop_Logic.SAnd (prop_for_bool_var_equality (apply2 fst_var (x1, x2)), + prop_for_bool_var_equality (apply2 snd_var (x1, x2))) val prop_for_assign_clause = Prop_Logic.exists o map prop_for_assign_literal @@ -530,9 +530,9 @@ fold (fn x => fn accum => if AList.defined (op =) asgs x then accum - else case (fst_var x, snd_var x) |> pairself assigns of + else case (fst_var x, snd_var x) |> apply2 assigns of (NONE, NONE) => accum - | bp => (x, annotation_from_bools (pairself (the_default false) bp)) + | bp => (x, annotation_from_bools (apply2 (the_default false) bp)) :: accum) (max_var downto 1) asgs diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Nitpick/nitpick_nut.ML --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Wed Nov 26 20:05:34 2014 +0100 @@ -765,7 +765,7 @@ else if is_Cst True u2 then u1 else raise SAME () | Eq => - (case pairself (is_Cst Unrep) (u1, u2) of + (case apply2 (is_Cst Unrep) (u1, u2) of (true, true) => unknown_boolean T R | (false, false) => raise SAME () | _ => if forall (is_opt_rep o rep_of) [u1, u2] then raise SAME () diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Nitpick/nitpick_preproc.ML --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Wed Nov 26 20:05:34 2014 +0100 @@ -173,10 +173,9 @@ end and do_equals new_Ts old_Ts s0 T0 t1 t2 = let - val (t1, t2) = pairself (do_term new_Ts old_Ts Neut) (t1, t2) - val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2) - val T = if def then T1 - else [T1, T2] |> sort (int_ord o pairself size_of_typ) |> hd + val (t1, t2) = apply2 (do_term new_Ts old_Ts Neut) (t1, t2) + val (T1, T2) = apply2 (curry fastype_of1 new_Ts) (t1, t2) + val T = if def then T1 else [T1, T2] |> sort (int_ord o apply2 size_of_typ) |> hd in list_comb (Const (s0, T --> T --> body_type T0), map2 (coerce_term hol_ctxt new_Ts T) [T1, T2] [t1, t2]) @@ -608,9 +607,9 @@ | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) => do_quantifier s0 T0 s1 T1 t1 | @{const HOL.conj} $ t1 $ t2 => - s_conj (pairself (aux ss Ts js skolemizable polar) (t1, t2)) + s_conj (apply2 (aux ss Ts js skolemizable polar) (t1, t2)) | @{const HOL.disj} $ t1 $ t2 => - s_disj (pairself (aux ss Ts js skolemizable polar) (t1, t2)) + s_disj (apply2 (aux ss Ts js skolemizable polar) (t1, t2)) | @{const HOL.implies} $ t1 $ t2 => @{const HOL.implies} $ aux ss Ts js skolemizable (flip_polarity polar) t1 $ aux ss Ts js skolemizable polar t2 @@ -758,7 +757,7 @@ val _ = not (null fixed_js) orelse raise SAME () val fixed_args = filter_indices fixed_js args val vars = fold Term.add_vars fixed_args [] - |> sort (Term_Ord.fast_indexname_ord o pairself fst) + |> sort (Term_Ord.fast_indexname_ord o apply2 fst) val bound_js = fold (fn t => fn js => add_loose_bnos (t, 0, js)) fixed_args [] |> sort int_ord @@ -811,11 +810,11 @@ fun special_congruence_axiom T (js1, ts1, x1) (js2, ts2, x2) = let - val (bounds1, bounds2) = pairself (map Var o special_bounds) (ts1, ts2) + val (bounds1, bounds2) = apply2 (map Var o special_bounds) (ts1, ts2) val Ts = binder_types T val max_j = fold (fold Integer.max) [js1, js2] ~1 val (eqs, (args1, args2)) = - fold (fn j => case pairself (fn ps => AList.lookup (op =) ps j) + fold (fn j => case apply2 (fn ps => AList.lookup (op =) ps j) (js1 ~~ ts1, js2 ~~ ts2) of (SOME t1, SOME t2) => apfst (cons (t1, t2)) | (SOME t1, NONE) => apsnd (apsnd (cons t1)) @@ -823,7 +822,7 @@ | (NONE, NONE) => let val v = Var ((cong_var_prefix ^ nat_subscript j, 0), nth Ts j) in - apsnd (pairself (cons v)) + apsnd (apply2 (cons v)) end) (max_j downto 0) ([], ([], [])) in Logic.list_implies (eqs |> filter_out (op aconv) |> distinct (op =) @@ -849,7 +848,7 @@ | do_pass_1 T skipped _ [] = do_pass_2 T skipped | do_pass_1 T skipped all (z :: zs) = case filter (is_more_specific z) all - |> sort (int_ord o pairself generality) of + |> sort (int_ord o apply2 generality) of [] => do_pass_1 T (z :: skipped) all zs | (z' :: _) => cons (special_congruence_axiom T z z') #> do_pass_1 T skipped all zs @@ -883,7 +882,7 @@ fun all_table_entries table = Symtab.fold (append o snd) table [] fun extra_table tables s = - Symtab.make [(s, pairself all_table_entries tables |> op @)] + Symtab.make [(s, apply2 all_table_entries tables |> op @)] fun eval_axiom_for_term j t = Logic.mk_equals (Const (eval_prefix ^ string_of_int j, fastype_of t), t) @@ -1199,7 +1198,7 @@ val (costly_boundss, (j, js)) = js |> map (`(merge costly_boundss o single)) |> sort (int_ord - o pairself (Integer.sum o map snd o fst)) + o apply2 (Integer.sum o map snd o fst)) |> split_list |>> hd ||> pairf hd tl in j :: heuristically_best_permutation costly_boundss js @@ -1208,7 +1207,7 @@ if length Ts <= quantifier_cluster_threshold then all_permutations (index_seq 0 num_Ts) |> map (`(cost (t_boundss ~~ t_costs))) - |> sort (int_ord o pairself fst) |> hd |> snd + |> sort (int_ord o apply2 fst) |> hd |> snd else heuristically_best_permutation (t_boundss ~~ t_costs) (index_seq 0 num_Ts) diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Nitpick/nitpick_rep.ML --- a/src/HOL/Tools/Nitpick/nitpick_rep.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML Wed Nov 26 20:05:34 2014 +0100 @@ -213,7 +213,7 @@ | min_rep (Struct Rs) _ = Struct Rs | min_rep _ (Struct Rs) = Struct Rs | min_rep (R1 as Func (R11, R12)) (R2 as Func (R21, R22)) = - (case pairself is_opt_rep (R12, R22) of + (case apply2 is_opt_rep (R12, R22) of (true, false) => R1 | (false, true) => R2 | _ => if R11 = R21 then Func (R11, min_rep R12 R22) diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Nitpick/nitpick_scope.ML --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Wed Nov 26 20:05:34 2014 +0100 @@ -214,7 +214,7 @@ #data_types s1 = #data_types s2 andalso #card_assigns s1 = #card_assigns s2 fun scope_less_eq (s1 : scope) (s2 : scope) = - (s1, s2) |> pairself (map snd o #card_assigns) |> op ~~ |> forall (op <=) + (s1, s2) |> apply2 (map snd o #card_assigns) |> op ~~ |> forall (op <=) fun rank_of_row (_, ks) = length ks @@ -293,7 +293,7 @@ k :: ks |> map (fn k => (k + linearity) * (k + linearity)) |> Integer.sum in - all_combinations #> map (`cost) #> sort (int_ord o pairself fst) #> map snd + all_combinations #> map (`cost) #> sort (int_ord o apply2 fst) #> map snd end fun is_self_recursive_constr_type T = @@ -449,7 +449,7 @@ val xs = binarized_and_boxed_data_type_constrs hol_ctxt binarize T val self_recs = map (is_self_recursive_constr_type o snd) xs val (num_self_recs, num_non_self_recs) = - List.partition I self_recs |> pairself length + List.partition I self_recs |> apply2 length val self_rec = num_self_recs > 0 fun is_complete facto = has_exact_card hol_ctxt facto finitizable_dataTs card_assigns T @@ -467,7 +467,7 @@ val constrs = fold_rev (add_constr_spec desc (not co) card sum_dom_cards num_self_recs num_non_self_recs) - (sort (bool_ord o swap o pairself fst) (self_recs ~~ xs)) [] + (sort (bool_ord o swap o apply2 fst) (self_recs ~~ xs)) [] in {typ = T, card = card, co = co, self_rec = self_rec, complete = complete, concrete = concrete, deep = deep, constrs = constrs} diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Old_Datatype/old_datatype_aux.ML --- a/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML Wed Nov 26 20:05:34 2014 +0100 @@ -396,7 +396,7 @@ fun max xs = fold max_inf xs (SOME 0); val (_, _, constrs) = the (AList.lookup (op =) descr i); val xs = - sort (int_ord o pairself snd) + sort (int_ord o apply2 snd) (map_filter (fn (s, dts) => Option.map (pair s) (max (map (arg_nonempty o strip_dtyp) dts))) constrs) in if null xs then NONE else SOME (hd xs) end; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Old_Datatype/old_datatype_data.ML --- a/src/HOL/Tools/Old_Datatype/old_datatype_data.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Old_Datatype/old_datatype_data.ML Wed Nov 26 20:05:34 2014 +0100 @@ -162,7 +162,7 @@ val k = find_index (fn (_, (_, dTs, _)) => not (forall is_DtTFree dTs)) descr; val protoTs as (dataTs, _) = chop k descr - |> (pairself o map) + |> (apply2 o map) (fn (_, (tyco, dTs, _)) => (tyco, map (Old_Datatype_Aux.typ_of_dtyp descr) dTs)); val tycos = map fst dataTs; @@ -172,7 +172,7 @@ error ("Type constructors " ^ commas_quote raw_tycos ^ " do not belong exhaustively to one mutually recursive old-style datatype"); - val (Ts, Us) = (pairself o map) Type protoTs; + val (Ts, Us) = apply2 (map Type) protoTs; val names = map Long_Name.base_name tycos; val (auxnames, _) = diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Predicate_Compile/core_data.ML --- a/src/HOL/Tools/Predicate_Compile/core_data.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Predicate_Compile/core_data.ML Wed Nov 26 20:05:34 2014 +0100 @@ -234,7 +234,7 @@ let fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t) fun inst_of_matches tts = fold (Pattern.match thy) tts (Vartab.empty, Vartab.empty) - |> snd |> Vartab.dest |> map (pairself (cterm_of thy) o term_pair_of) + |> snd |> Vartab.dest |> map (apply2 (cterm_of thy) o term_pair_of) val (cases, (eqs, prems)) = apsnd (chop (nargs - nparams)) (chop n prems) val case_th = rewrite_rule ctxt (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1)) @@ -445,8 +445,8 @@ let (* thm refl is a dummy thm *) val modes = map fst compilations - val (needs_random, non_random_modes) = pairself (map fst) - (List.partition (fn (_, (_, random)) => random) compilations) + val (needs_random, non_random_modes) = + apply2 (map fst) (List.partition (fn (_, (_, random)) => random) compilations) val non_random_dummys = map (rpair "dummy") non_random_modes val all_dummys = map (rpair "dummy") modes val dummy_function_names = diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Nov 26 20:05:34 2014 +0100 @@ -350,7 +350,7 @@ else if eq_mode (m, Output) then (NONE, SOME t) else raise Fail "split_map_mode: mode and term do not match" in - (pairself (map_filter I) o split_list) (map2 split_arg_mode' (strip_fun_mode mode) ts) + (apply2 (map_filter I) o split_list) (map2 split_arg_mode' (strip_fun_mode mode) ts) end (* splits mode and maps function to higher-order argument types *) @@ -368,7 +368,7 @@ | split_arg_mode' Output T = (NONE, SOME T) | split_arg_mode' _ _ = raise Fail "split_modeT': mode and type do not match" in - (pairself (map_filter I) o split_list) (map2 split_arg_mode' (strip_fun_mode mode) Ts) + (apply2 (map_filter I) o split_list) (map2 split_arg_mode' (strip_fun_mode mode) Ts) end fun split_mode mode ts = split_map_mode (fn _ => fn _ => (NONE, NONE)) mode ts @@ -400,7 +400,7 @@ | split_arg_mode Output T = ([], [T]) | split_arg_mode _ _ = raise Fail "split_modeT: mode and type do not match" in - (pairself flat o split_list) (map2 split_arg_mode (strip_fun_mode mode) Ts) + (apply2 flat o split_list) (map2 split_arg_mode (strip_fun_mode mode) Ts) end fun string_of_mode mode = diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Nov 26 20:05:34 2014 +0100 @@ -210,7 +210,7 @@ | check _ _ = false fun check_consistent_modes ms = if forall (fn Fun _ => true | _ => false) ms then - pairself check_consistent_modes (split_list (map (fn Fun (m1, m2) => (m1, m2)) ms)) + apply2 check_consistent_modes (split_list (map (fn Fun (m1, m2) => (m1, m2)) ms)) |> (fn (res1, res2) => res1 andalso res2) else if forall (fn Input => true | Output => true | Pair _ => true | _ => false) ms then true @@ -864,7 +864,7 @@ let fun select_best_switch moded_clauses input_position best_switch = let - val ord = option_ord (rev_order o int_ord o (pairself (length o snd o snd))) + val ord = option_ord (rev_order o int_ord o (apply2 (length o snd o snd))) val partition = partition_clause ctxt input_position moded_clauses val switch = if (length (fst partition) > 1) then SOME (input_position, partition) else NONE in diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Wed Nov 26 20:05:34 2014 +0100 @@ -21,7 +21,7 @@ structure Fun_Pred = Theory_Data ( type T = (term * term) Item_Net.T; - val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst); + val empty : T = Item_Net.init (op aconv o apply2 fst) (single o fst); val extend = I; val merge = Item_Net.merge; ) @@ -295,7 +295,7 @@ map Drule.export_without_context (filter (Predicate_Compile_Aux.is_intro predname) intrs))) dst_prednames val thy'' = Fun_Pred.map - (fold Item_Net.update (map (pairself Logic.varify_global) + (fold Item_Net.update (map (apply2 Logic.varify_global) (dst_funs ~~ dst_preds))) thy' fun functional_mode_of T = list_fun_mode (replicate (length (binder_types T)) Input @ [Output]) diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Wed Nov 26 20:05:34 2014 +0100 @@ -19,7 +19,7 @@ structure Specialisations = Theory_Data ( type T = (term * term) Item_Net.T - val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst) + val empty : T = Item_Net.init (op aconv o apply2 fst) (single o fst) val extend = I val merge = Item_Net.merge ) @@ -49,7 +49,7 @@ (Var _, []) => (true, true) | (Free _, []) => (true, true) | (Const (@{const_name Pair}, _), ts) => - pairself (forall I) (split_list (map check ts)) + apply2 (forall I) (split_list (map check ts)) | (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of (SOME (i, Tname), Type (Tname', _)) => (false, diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Qelim/cooper.ML Wed Nov 26 20:05:34 2014 +0100 @@ -694,7 +694,7 @@ val (_, oracle) = Context.>>> (Context.map_theory_result (Thm.add_oracle (@{binding cooper}, (fn (ctxt, t) => - (Thm.cterm_of (Proof_Context.theory_of ctxt) o Logic.mk_equals o pairself HOLogic.mk_Trueprop) + (Thm.cterm_of (Proof_Context.theory_of ctxt) o Logic.mk_equals o apply2 HOLogic.mk_Trueprop) (t, procedure t))))); val comp_ss = diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Quickcheck/quickcheck_common.ML --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Wed Nov 26 20:05:34 2014 +0100 @@ -417,7 +417,7 @@ else case perhaps_constrain thy insts vs of SOME constrain => instantiate config descr (map constrain vs) tycos prfx (names, auxnames) - ((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy + ((apply2 o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy | NONE => thy end; @@ -491,7 +491,7 @@ Type (@{type_name fun}, [T1, T2]) => (case try dest_fun_upds t of SOME (tps, t) => - (map (pairself post_process_term) tps, map_Abs post_process_term t) + (map (apply2 post_process_term) tps, map_Abs post_process_term t) |> (case T2 of @{typ bool} => (case t of diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/SMT/smt_normalize.ML --- a/src/HOL/Tools/SMT/smt_normalize.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/SMT/smt_normalize.ML Wed Nov 26 20:05:34 2014 +0100 @@ -171,7 +171,7 @@ if has_all_vars vs (Thm.term_of ct) then (case Thm.term_of ct of _ $ _ => - (case pairself (minimal_pats vs) (Thm.dest_comb ct) of + (case apply2 (minimal_pats vs) (Thm.dest_comb ct) of ([], []) => [[ct]] | (ctss, ctss') => union (eq_set (op aconvc)) ctss ctss') | _ => []) @@ -189,7 +189,7 @@ fun mk_pat ct = Thm.apply (SMT_Util.instT' ct pat) ct fun mk_clist T = - pairself (Thm.cterm_of @{theory}) (SMT_Util.symb_cons_const T, SMT_Util.symb_nil_const T) + apply2 (Thm.cterm_of @{theory}) (SMT_Util.symb_cons_const T, SMT_Util.symb_nil_const T) fun mk_list (ccons, cnil) f cts = fold_rev (Thm.mk_binop ccons o f) cts cnil val mk_pat_list = mk_list (mk_clist @{typ pattern}) val mk_mpat_list = mk_list (mk_clist @{typ "pattern symb_list"}) diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/SMT/smtlib_interface.ML --- a/src/HOL/Tools/SMT/smtlib_interface.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML Wed Nov 26 20:05:34 2014 +0100 @@ -149,7 +149,7 @@ |> fold (Buffer.add o enclose "(declare-sort " " 0)\n") (sort fast_string_ord sorts) |> fold sdtyp (AList.coalesce (op =) dtyps) |> fold (Buffer.add o enclose "(declare-fun " ")\n" o string_of_fun) - (sort (fast_string_ord o pairself fst) funcs) + (sort (fast_string_ord o apply2 fst) funcs) |> fold (fn (i, t) => Buffer.add (enclose "(assert " ")\n" (SMTLIB.str_of (named_sterm (assert_name_of_index i) (tree_of_sterm 0 t))))) (map_index I ts) |> Buffer.add "(check-sat)\n" diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/SMT/z3_proof.ML --- a/src/HOL/Tools/SMT/z3_proof.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/SMT/z3_proof.ML Wed Nov 26 20:05:34 2014 +0100 @@ -221,7 +221,7 @@ fun with_quant pred i (Const q1 $ Abs (_, T1, t1), Const q2 $ Abs (_, T2, t2)) = if pred q1 q2 andalso T1 = T2 then let val t = Var (("", i), T1) - in SOME (pairself Term.subst_bound ((t, t1), (t, t2))) end + in SOME (apply2 Term.subst_bound ((t, t1), (t, t2))) end else NONE | with_quant _ _ _ = NONE diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/SMT/z3_replay_literals.ML --- a/src/HOL/Tools/SMT/z3_replay_literals.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/SMT/z3_replay_literals.ML Wed Nov 26 20:05:34 2014 +0100 @@ -254,7 +254,7 @@ | NONE => (case lookup_rule t of (rewrite, SOME lit) => (s, rewrite lit) - | (_, NONE) => (s, comp (pairself join1 (dest t))))) + | (_, NONE) => (s, comp (apply2 join1 (dest t))))) in snd (join1 (if is_conj then (false, t) else (true, t))) end @@ -289,7 +289,7 @@ SOME rs => extract_lit thm rs | NONE => the (Termtab.get_first contra_lits rules) - |> pairself (extract_lit thm) + |> apply2 (extract_lit thm) |> (fn (nlit, plit) => nlit COMP (plit COMP contra_rule))) end diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Nov 26 20:05:34 2014 +0100 @@ -82,7 +82,7 @@ (used_facts, (case AList.lookup (op =) ress preferred_meth of SOME play => (preferred_meth, play) - | NONE => hd (sort (play_outcome_ord o pairself snd) (rev ress)))) + | NONE => hd (sort (play_outcome_ord o apply2 snd) (rev ress)))) | try_methss ress (meths :: methss) = let fun mk_step fact_names meths = diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed Nov 26 20:05:34 2014 +0100 @@ -348,7 +348,7 @@ | normalize_eq t = t fun if_thm_before th th' = - if Theory.subthy (pairself Thm.theory_of_thm (th, th')) then th else th' + if Theory.subthy (apply2 Thm.theory_of_thm (th, th')) then th else th' (* Hack: Conflate the facts about a class as seen from the outside with the corresponding low-level facts, so that MaSh can learn from the low-level proofs. *) @@ -373,7 +373,7 @@ fun fact_distinct eq facts = fold (fn fact as (_, th) => - Net.insert_term_safe (eq o pairself (normalize_eq o prop_of o snd)) + Net.insert_term_safe (eq o apply2 (normalize_eq o prop_of o snd)) (normalize_eq (prop_of th), fact)) facts Net.empty |> Net.entries @@ -542,7 +542,7 @@ o fact_of_ref ctxt keywords chained css) add else let - val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) + val (add, del) = apply2 (Attrib.eval_thms ctxt) (add, del) val facts = all_facts ctxt false ho_atp keywords add chained css |> filter_out ((member Thm.eq_thm_prop del orf diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML Wed Nov 26 20:05:34 2014 +0100 @@ -145,7 +145,7 @@ val (typing_spots, tvar_count_tab) = Var_Set_Tab.fold (fn kv as (k, _) => apfst (cons kv) #> apsnd (update_count 1 k)) typing_spot_tab ([], Vartab.empty) - |>> sort_distinct (rev_order o cost_ord o pairself snd) + |>> sort_distinct (rev_order o cost_ord o apply2 snd) in fold drop_superfluous typing_spots ([], tvar_count_tab) |> fst end diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Wed Nov 26 20:05:34 2014 +0100 @@ -195,7 +195,7 @@ let val cand_key = apfst (length o get_successors) val cand_ord = - prod_ord int_ord (prod_ord (int_ord o swap) (int_ord o swap)) o pairself cand_key + prod_ord int_ord (prod_ord (int_ord o swap) (int_ord o swap)) o apply2 cand_key fun pop_next_candidate [] = (NONE, []) | pop_next_candidate (cands as (cand :: cands')) = diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Wed Nov 26 20:05:34 2014 +0100 @@ -104,7 +104,7 @@ fun resolve_fact_names ctxt names = (names |>> map string_of_label - |> pairself (maps (thms_of_name ctxt))) + |> apply2 (maps (thms_of_name ctxt))) handle ERROR msg => error ("preplay error: " ^ msg) fun thm_of_proof ctxt (Proof (fixed_frees, assms, steps)) = @@ -176,7 +176,7 @@ val meths = proof_methods_of_isar_step step |> subtract (op =) hopeless in par_list_map_filter_with_timeout get_time min_preplay_timeout timeout0 preplay meths - |> sort (play_outcome_ord o pairself snd) + |> sort (play_outcome_ord o apply2 snd) end type isar_preplay_data = (proof_method * play_outcome Lazy.lazy) list Canonical_Label_Tab.table @@ -188,7 +188,7 @@ | add_preplay_outcomes _ Play_Failed = Play_Failed | add_preplay_outcomes (Played time1) (Played time2) = Played (Time.+ (time1, time2)) | add_preplay_outcomes play1 play2 = - Play_Timed_Out (Time.+ (pairself time_of_play (play1, play2))) + Play_Timed_Out (Time.+ (apply2 time_of_play (play1, play2))) fun set_preplay_outcomes_of_isar_step ctxt timeout preplay_data (step as Prove (_, _, l, _, _, _, meths, _)) meths_outcomes0 = @@ -207,7 +207,7 @@ fun get_best_method_outcome force = tap (List.app (K () o Lazy.future Future.default_params o snd)) (* could be parallelized *) #> map (apsnd force) - #> sort (play_outcome_ord o pairself snd) + #> sort (play_outcome_ord o apply2 snd) #> hd fun forced_intermediate_preplay_outcome_of_isar_step preplay_data l = diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Wed Nov 26 20:05:34 2014 +0100 @@ -81,7 +81,7 @@ val have_prefix = "f" fun label_ord ((s1, i1), (s2, i2)) = - (case int_ord (pairself String.size (s1, s2)) of + (case int_ord (apply2 String.size (s1, s2)) of EQUAL => (case string_ord (s1, s2) of EQUAL => int_ord (i1, i2) diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed Nov 26 20:05:34 2014 +0100 @@ -187,7 +187,7 @@ fun weight_of fact = mess |> map_filter (score_in fact) |> scaled_avg in fold (union fact_eq o map fst o take max_facts o fst o snd) mess [] - |> map (`weight_of) |> sort (int_ord o pairself fst o swap) + |> map (`weight_of) |> sort (int_ord o apply2 fst o swap) |> map snd |> take max_facts end @@ -363,7 +363,7 @@ if at = num_facts then acc else ret (at + 1) (Array.sub (posterior, at) :: acc) in select_visible_facts 100000.0 posterior visible_facts; - sort_array_suffix (Real.compare o pairself snd) max_suggs posterior; + sort_array_suffix (Real.compare o apply2 snd) max_suggs posterior; ret (Integer.max 0 (num_facts - max_suggs)) [] end @@ -396,7 +396,7 @@ end val _ = List.app do_feat goal_feats - val _ = sort_array_suffix (Real.compare o pairself snd) num_facts overlaps_sqr + val _ = sort_array_suffix (Real.compare o apply2 snd) num_facts overlaps_sqr val no_recommends = Unsynchronized.ref 0 val recommends = Array.tabulate (num_facts, rpair 0.0) val age = Unsynchronized.ref 500000000.0 @@ -438,7 +438,7 @@ while1 (); while2 (); select_visible_facts 1000000000.0 recommends visible_facts; - sort_array_suffix (Real.compare o pairself snd) max_suggs recommends; + sort_array_suffix (Real.compare o apply2 snd) max_suggs recommends; ret [] (Integer.max 0 (num_facts - max_suggs)) end @@ -777,24 +777,24 @@ else if Theory.subthy (swap p) then GREATER else - (case int_ord (pairself (length o Theory.ancestors_of) p) of - EQUAL => string_ord (pairself Context.theory_name p) + (case int_ord (apply2 (length o Theory.ancestors_of) p) of + EQUAL => string_ord (apply2 Context.theory_name p) | order => order) fun crude_thm_ord p = - (case crude_theory_ord (pairself theory_of_thm p) of + (case crude_theory_ord (apply2 theory_of_thm p) of EQUAL => (* The hack below is necessary because of odd dependencies that are not reflected in the theory comparison. *) - let val q = pairself nickname_of_thm p in + let val q = apply2 nickname_of_thm p in (* Hack to put "xxx_def" before "xxxI" and "xxxE" *) - (case bool_ord (pairself (String.isSuffix "_def") (swap q)) of + (case bool_ord (apply2 (String.isSuffix "_def") (swap q)) of EQUAL => string_ord q | ord => ord) end | ord => ord) -val thm_less_eq = Theory.subthy o pairself theory_of_thm +val thm_less_eq = Theory.subthy o apply2 theory_of_thm fun thm_less p = thm_less_eq p andalso not (thm_less_eq (swap p)) val freezeT = Type.legacy_freeze_type @@ -1154,7 +1154,7 @@ val algorithm = the_mash_algorithm () val facts = facts - |> rev_sort_list_prefix (crude_thm_ord o pairself snd) + |> rev_sort_list_prefix (crude_thm_ord o apply2 snd) (Int.max (num_extra_feature_facts, max_proximity_facts)) val chained = filter (fn ((_, (scope, _)), _) => scope = Chained) facts @@ -1184,7 +1184,7 @@ val goal_feats = fold (union (eq_fst (op =))) [chained_feats, extra_feats] (map (rpair 1.0) goal_feats0) - |> debug ? sort (Real.compare o swap o pairself snd) + |> debug ? sort (Real.compare o swap o apply2 snd) val parents = maximal_wrt_access_graph access_G facts val visible_facts = map_filter (Symtab.lookup fact_tab) (Graph.all_preds access_G parents) @@ -1209,7 +1209,7 @@ val unknown = filter_out (is_fact_in_graph access_G o snd) facts in find_mash_suggestions ctxt max_suggs suggs facts chained unknown - |> pairself (map fact_of_raw_fact) + |> apply2 (map fact_of_raw_fact) end fun mash_unlearn () = (clear_state (); writeln "Reset MaSh.") @@ -1268,7 +1268,7 @@ let val thy = Proof_Context.theory_of ctxt val feats = features_of ctxt thy (Local, General) [t] - val facts = rev_sort_list_prefix (crude_thm_ord o pairself snd) 1 facts + val facts = rev_sort_list_prefix (crude_thm_ord o apply2 snd) 1 facts in map_state ctxt (fn {access_G, xtabs as ((num_facts0, _), _), ffds, freqs, dirty_facts} => @@ -1397,7 +1397,7 @@ else let val new_facts = facts - |> sort (crude_thm_ord o pairself snd) + |> sort (crude_thm_ord o apply2 snd) |> attach_parents_to_facts [] |> filter_out (is_in_access_G o snd) val (learns, (num_nontrivial, _, _)) = @@ -1444,7 +1444,7 @@ val old_facts = facts |> filter is_in_access_G |> map (`(priority_of o snd)) - |> sort (int_ord o pairself fst) + |> sort (int_ord o apply2 fst) |> map snd val ((relearns, flops), (num_nontrivial, _, _)) = (([], []), (num_nontrivial, next_commit_time (), false)) @@ -1469,7 +1469,7 @@ val ctxt = ctxt |> Config.put instantiate_inducts false val facts = nearly_all_facts ctxt false fact_override Keyword.empty_keywords css chained [] @{prop True} - |> sort (crude_thm_ord o pairself snd o swap) + |> sort (crude_thm_ord o apply2 snd o swap) val num_facts = length facts val prover = hd provers diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Wed Nov 26 20:05:34 2014 +0100 @@ -361,7 +361,7 @@ Real.ceil (Math.pow (max_imperfect, Math.pow (Real.fromInt remaining_max / Real.fromInt max_facts, max_imperfect_exp))) val (perfect, imperfect) = candidates - |> sort (Real.compare o swap o pairself snd) + |> sort (Real.compare o swap o apply2 snd) |> take_prefix (fn (_, w) => w > 0.99999) val ((accepts, more_rejects), rejects) = chop max_imperfect imperfect |>> append perfect |>> chop remaining_max diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Wed Nov 26 20:05:34 2014 +0100 @@ -149,11 +149,11 @@ | string_of_play_outcome Play_Failed = "failed" fun play_outcome_ord (Played time1, Played time2) = - int_ord (pairself Time.toMilliseconds (time1, time2)) + int_ord (apply2 Time.toMilliseconds (time1, time2)) | play_outcome_ord (Played _, _) = LESS | play_outcome_ord (_, Played _) = GREATER | play_outcome_ord (Play_Timed_Out time1, Play_Timed_Out time2) = - int_ord (pairself Time.toMilliseconds (time1, time2)) + int_ord (apply2 Time.toMilliseconds (time1, time2)) | play_outcome_ord (Play_Timed_Out _, _) = LESS | play_outcome_ord (_, Play_Timed_Out _) = GREATER | play_outcome_ord (Play_Failed, Play_Failed) = EQUAL diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Wed Nov 26 20:05:34 2014 +0100 @@ -178,7 +178,7 @@ | _ => let val (sup_r0, (l, result)) = min depth result (sup @ r0) l0 - val (sup, r0) = (sup, r0) |> pairself (filter_used_facts true (map fst sup_r0)) + val (sup, r0) = (sup, r0) |> apply2 (filter_used_facts true (map fst sup_r0)) val (sup_l, (r, result)) = min depth result (sup @ l) r0 val sup = sup |> filter_used_facts true (map fst sup_l) in (sup, (l @ r, result)) end)) diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Nov 26 20:05:34 2014 +0100 @@ -115,7 +115,7 @@ (case try Thm.proof_body_of th of NONE => NONE | SOME body => - let val map_names = (case name_tabs of SOME p => pairself Symtab.lookup p | NONE => `I SOME) in + let val map_names = (case name_tabs of SOME p => apply2 Symtab.lookup p | NONE => `I SOME) in SOME (fold_body_thm max_thms (Thm.get_name_hint th) map_names (Proofterm.strip_thm body)) handle TOO_MANY () => NONE end) diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/TFL/rules.ML --- a/src/HOL/Tools/TFL/rules.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/TFL/rules.ML Wed Nov 26 20:05:34 2014 +0100 @@ -389,7 +389,7 @@ fun IT_EXISTS blist th = let val thy = Thm.theory_of_thm th val tych = cterm_of thy - val blist' = map (pairself Thm.term_of) blist + val blist' = map (apply2 Thm.term_of) blist fun ex v M = cterm_of thy (USyntax.mk_exists{Bvar=v,Body = M}) in diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/TFL/tfl.ML --- a/src/HOL/Tools/TFL/tfl.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/TFL/tfl.ML Wed Nov 26 20:05:34 2014 +0100 @@ -333,7 +333,7 @@ {path=[a], rows=rows} val patts1 = map (fn (_,tag,[pat]) => (pat,tag)) patts handle Match => mk_functional_err "error in pattern-match translation" - val patts2 = Library.sort (Library.int_ord o Library.pairself row_of_pat) patts1 + val patts2 = Library.sort (Library.int_ord o apply2 row_of_pat) patts1 val finals = map row_of_pat patts2 val originals = map (row_of_pat o #2) rows val dummy = case (subtract (op =) finals originals) diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/Transfer/transfer.ML --- a/src/HOL/Tools/Transfer/transfer.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Transfer/transfer.ML Wed Nov 26 20:05:34 2014 +0100 @@ -48,7 +48,7 @@ (** Theory Data **) -val compound_xhs_empty_net = Item_Net.init (Thm.eq_thm_prop o pairself snd) (single o fst); +val compound_xhs_empty_net = Item_Net.init (Thm.eq_thm_prop o apply2 snd) (single o fst); val rewr_rules = Item_Net.init Thm.eq_thm_prop (single o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.concl_of); diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/code_evaluation.ML --- a/src/HOL/Tools/code_evaluation.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/code_evaluation.ML Wed Nov 26 20:05:34 2014 +0100 @@ -62,7 +62,7 @@ val t = list_comb (Const (c, tys ---> ty), map Free (Name.invent_names Name.context "a" tys)); val (arg, rhs) = - pairself (Thm.cterm_of thy o Logic.unvarify_types_global o Logic.varify_global) + apply2 (Thm.cterm_of thy o Logic.unvarify_types_global o Logic.varify_global) (t, map_aterms (fn t as Free (_, ty) => HOLogic.mk_term_of ty t | t => t) (HOLogic.reflect_term t)); diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/coinduction.ML --- a/src/HOL/Tools/coinduction.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/coinduction.ML Wed Nov 26 20:05:34 2014 +0100 @@ -65,8 +65,8 @@ |> fold Variable.declare_thm (raw_thm :: prems); val thm_concl = Thm.cprop_of raw_thm |> strip_imp_concl; val (rhoTs, rhots) = Thm.match (thm_concl, concl) - |>> map (pairself typ_of) - ||> map (pairself term_of); + |>> map (apply2 typ_of) + ||> map (apply2 term_of); val xs = hd (Thm.prems_of raw_thm) |> HOLogic.dest_Trueprop |> strip_comb |> snd |> map (subst_atomic_types rhoTs); val raw_eqs = map (fn x => (x, AList.lookup op aconv rhots x |> the)) xs; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/datatype_realizer.ML --- a/src/HOL/Tools/datatype_realizer.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/datatype_realizer.ML Wed Nov 26 20:05:34 2014 +0100 @@ -106,7 +106,7 @@ (map (fn ((((i, _), T), U), tname) => make_pred i U T (mk_proj i is r) (Free (tname, T))) (descr ~~ recTs ~~ rec_result_Ts ~~ tnames))); - val inst = map (pairself cert) (map head_of (HOLogic.dest_conj + val inst = map (apply2 cert) (map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct))) ~~ ps); val thm = diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/functor.ML --- a/src/HOL/Tools/functor.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/functor.ML Wed Nov 26 20:05:34 2014 +0100 @@ -149,8 +149,8 @@ val lhs1 = list_comb (head, map (HOLogic.id_const) arg_Ts); val lhs2 = list_comb (head, map (fn arg_T => Abs ("x", arg_T, Bound 0)) arg_Ts); val rhs = HOLogic.id_const T; - val (id_prop, identity_prop) = pairself - (HOLogic.mk_Trueprop o HOLogic.mk_eq o rpair rhs) (lhs1, lhs2); + val (id_prop, identity_prop) = + apply2 (HOLogic.mk_Trueprop o HOLogic.mk_eq o rpair rhs) (lhs1, lhs2); fun prove_identity ctxt id_thm = Goal.prove_sorry ctxt [] [] identity_prop (K (ALLGOALS (Method.insert_tac [id_thm] THEN' Simplifier.asm_lr_simp_tac (put_simpset identity_ss ctxt)))); @@ -206,11 +206,12 @@ fun bad_typ () = error ("Bad mapper type: " ^ Syntax.string_of_typ ctxt T); val (Ts, T1, T2) = split_mapper_typ tyco T handle List.Empty => bad_typ (); - val _ = pairself - ((fn tyco' => if tyco' = tyco then () else bad_typ ()) o fst o dest_Type) (T1, T2) - handle TYPE _ => bad_typ (); - val (vs1, vs2) = pairself (map dest_TFree o snd o dest_Type) (T1, T2) - handle TYPE _ => bad_typ (); + val _ = + apply2 ((fn tyco' => if tyco' = tyco then () else bad_typ ()) o fst o dest_Type) (T1, T2) + handle TYPE _ => bad_typ (); + val (vs1, vs2) = + apply2 (map dest_TFree o snd o dest_Type) (T1, T2) + handle TYPE _ => bad_typ (); val _ = if has_duplicates (eq_fst (op =)) (vs1 @ vs2) then bad_typ () else (); fun check_variance_pair (var1 as (_, sort1), var2 as (_, sort2)) = @@ -239,7 +240,7 @@ let val typ_instance = Sign.typ_instance (Context.theory_of context); val mapper' = Morphism.term phi mapper; - val T_T' = pairself fastype_of (mapper, mapper'); + val T_T' = apply2 fastype_of (mapper, mapper'); val vars = Term.add_vars mapper' []; in if null vars andalso typ_instance T_T' andalso typ_instance (swap T_T') diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/hologic.ML --- a/src/HOL/Tools/hologic.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/hologic.ML Wed Nov 26 20:05:34 2014 +0100 @@ -205,7 +205,7 @@ fun conj_intr thP thQ = let - val (P, Q) = pairself (Object_Logic.dest_judgment o Thm.cprop_of) (thP, thQ) + val (P, Q) = apply2 (Object_Logic.dest_judgment o Thm.cprop_of) (thP, thQ) handle CTERM (msg, _) => raise THM (msg, 0, [thP, thQ]); val inst = Thm.instantiate ([], [(@{cpat "?P::bool"}, P), (@{cpat "?Q::bool"}, Q)]); in Drule.implies_elim_list (inst @{thm conjI}) [thP, thQ] end; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/inductive_realizer.ML Wed Nov 26 20:05:34 2014 +0100 @@ -262,7 +262,7 @@ val vs1 = map Var (filter_out (fn ((a, _), _) => member (op =) rvs a) xs); val rlzvs = rev (Term.add_vars (prop_of rrule) []); val vs2 = map (fn (ixn, _) => Var (ixn, (the o AList.lookup (op =) rlzvs) ixn)) xs; - val rs = map Var (subtract (op = o pairself fst) xs rlzvs); + val rs = map Var (subtract (op = o apply2 fst) xs rlzvs); val rlz' = fold_rev Logic.all rs (prop_of rrule) in (name, (vs, if rt = Extraction.nullt then rt else fold_rev lambda vs1 rt, @@ -340,7 +340,7 @@ val s' = Long_Name.base_name s; val T' = Logic.unvarifyT_global T; in (((s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end) - |> distinct (op = o pairself (#1 o #1)) + |> distinct (op = o apply2 (#1 o #1)) |> map (apfst (apfst (apfst Binding.name))) |> split_list; @@ -369,7 +369,7 @@ fun add_ind_realizer Ps thy = let - val vs' = rename (map (pairself (fst o fst o dest_Var)) + val vs' = rename (map (apply2 (fst o fst o dest_Var)) (params ~~ List.take (snd (strip_comb (HOLogic.dest_Trueprop (hd (prems_of (hd inducts))))), nparms))) vs; val rs = indrule_realizer thy induct raw_induct rsets params' @@ -491,7 +491,7 @@ let val (_, {intrs, induct, raw_induct, elims, ...}) = Inductive.the_inductive (Proof_Context.init_global thy) name; - val vss = sort (int_ord o pairself length) + val vss = sort (int_ord o apply2 length) (subsets (map fst (relevant_vars (concl_of (hd intrs))))) in fold_rev (add_ind_realizer rsets intrs induct raw_induct elims) vss thy diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/lin_arith.ML Wed Nov 26 20:05:34 2014 +0100 @@ -317,10 +317,9 @@ new | NONE => (case t of Abs (a, T, body) => - let val pairs' = map (pairself (incr_boundvars 1)) pairs + let val pairs' = map (apply2 (incr_boundvars 1)) pairs in Abs (a, T, subst_term pairs' body) end - | t1 $ t2 => - subst_term pairs t1 $ subst_term pairs t2 + | t1 $ t2 => subst_term pairs t1 $ subst_term pairs t2 | _ => t)); (* approximates the effect of one application of split_tac (followed by NNF *) diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/monomorph.ML --- a/src/HOL/Tools/monomorph.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/monomorph.ML Wed Nov 26 20:05:34 2014 +0100 @@ -159,7 +159,7 @@ fun instantiate thy subst = let - fun cert (ix, (S, T)) = pairself (Thm.ctyp_of thy) (TVar (ix, S), T) + fun cert (ix, (S, T)) = apply2 (Thm.ctyp_of thy) (TVar (ix, S), T) fun cert' subst = Vartab.fold (cons o cert) subst [] in Thm.instantiate (cert' subst, []) end @@ -287,15 +287,15 @@ fun size_of_subst subst = Vartab.fold (Integer.add o size_of_typ o snd o snd) subst 0 -fun subst_ord subst = int_ord (pairself size_of_subst subst) +fun subst_ord subst = int_ord (apply2 size_of_subst subst) fun instantiated_thms _ _ (Ground thm) = [(0, thm)] | instantiated_thms _ _ Ignored = [] | instantiated_thms max_thm_insts insts (Schematic {id, ...}) = Inttab.lookup_list insts id - |> (fn rthms => if length rthms <= max_thm_insts then rthms - else take max_thm_insts - (sort (prod_ord int_ord subst_ord o pairself fst) rthms)) + |> (fn rthms => + if length rthms <= max_thm_insts then rthms + else take max_thm_insts (sort (prod_ord int_ord subst_ord o apply2 fst) rthms)) |> map (apfst fst) fun monomorph schematic_consts_of ctxt rthms = diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/record.ML Wed Nov 26 20:05:34 2014 +0100 @@ -1475,7 +1475,7 @@ | [x] => (head_of x, false)); val rule'' = cterm_instantiate - (map (pairself cert) + (map (apply2 cert) (case rev params of [] => (case AList.lookup (op =) (Term.add_frees g []) s of @@ -1758,7 +1758,7 @@ fun mk_eq_refl thy = @{thm equal_refl} |> Thm.instantiate - ([pairself (ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], []) + ([apply2 (ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], []) |> Axclass.unoverload thy; val ensure_random_record = ensure_sort_record (@{sort random}, mk_random_eq); val ensure_exhaustive_record = diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/reification.ML --- a/src/HOL/Tools/reification.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/reification.ML Wed Nov 26 20:05:34 2014 +0100 @@ -231,7 +231,7 @@ val substt = let val ih = Drule.cterm_rule (Thm.instantiate (subst_ty, [])); - in map (pairself ih) (subst_ns @ subst_vs @ cts) end; + in map (apply2 ih) (subst_ns @ subst_vs @ cts) end; val th = (Drule.instantiate_normalize (subst_ty, substt) eq) RS sym; in (hd (Variable.export ctxt'' ctxt [th]), bds) end) handle Pattern.MATCH => tryeqs eqs (ct, ctxt) bds); @@ -279,7 +279,8 @@ let val (congs, bds) = mk_congs ctxt eqs; val congs = rearrange congs; - val (th, bds') = apfst mk_eq (divide_and_conquer' (decomp_reify (mk_decompatom eqs) congs) (ct, ctxt) bds); + val (th, bds') = + apfst mk_eq (divide_and_conquer' (decomp_reify (mk_decompatom eqs) congs) (ct, ctxt) bds); fun is_list_var (Var (_, t)) = can dest_listT t | is_list_var _ = false; val vars = th |> prop_of |> Logic.dest_equals |> snd @@ -287,7 +288,7 @@ val cert = cterm_of (Proof_Context.theory_of ctxt); val vs = map (fn v as Var (_, T) => (v, the (AList.lookup Type.could_unify bds' T) |> snd |> HOLogic.mk_list (dest_listT T))) vars; - val th' = Drule.instantiate_normalize ([], (map o pairself) cert vs) th; + val th' = Drule.instantiate_normalize ([], (map o apply2) cert vs) th; val th'' = Thm.symmetric (dereify ctxt [] (Thm.lhs_of th')); in Thm.transitive th'' th' end; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/rewrite_hol_proof.ML --- a/src/HOL/Tools/rewrite_hol_proof.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/rewrite_hol_proof.ML Wed Nov 26 20:05:34 2014 +0100 @@ -13,7 +13,7 @@ structure RewriteHOLProof : REWRITE_HOL_PROOF = struct -val rews = map (pairself (Proof_Syntax.proof_of_term @{theory} true) o +val rews = map (apply2 (Proof_Syntax.proof_of_term @{theory} true) o Logic.dest_equals o Logic.varify_global o Proof_Syntax.read_term @{theory} true propT) (** eliminate meta-equality rules **) diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/sat.ML --- a/src/HOL/Tools/sat.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/sat.ML Wed Nov 26 20:05:34 2014 +0100 @@ -128,7 +128,7 @@ fun merge xs [] = xs | merge [] ys = ys | merge (x :: xs) (y :: ys) = - (case (lit_ord o pairself fst) (x, y) of + (case lit_ord (apply2 fst (x, y)) of LESS => x :: merge xs (y :: ys) | EQUAL => x :: merge xs ys | GREATER => y :: merge (x :: xs) ys) @@ -139,7 +139,7 @@ | find_res_hyps (_, []) _ = raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, []) | find_res_hyps (h1 :: hyps1, h2 :: hyps2) acc = - (case (lit_ord o pairself fst) (h1, h2) of + (case lit_ord (apply2 fst (h1, h2)) of LESS => find_res_hyps (hyps1, h2 :: hyps2) (h1 :: acc) | EQUAL => let @@ -227,7 +227,7 @@ let val _ = cond_tracing ctxt (fn () => "Using original clause #" ^ string_of_int id) val raw = CNF.clause2raw_thm thm - val hyps = sort (lit_ord o pairself fst) (map_filter (fn chyp => + val hyps = sort (lit_ord o apply2 fst) (map_filter (fn chyp => Option.map (rpair chyp) (index_of_literal chyp)) (#hyps (Thm.crep_thm raw))) val clause = (raw, hyps) val _ = Array.update (clauses, id, RAW_CLAUSE clause) @@ -304,7 +304,7 @@ (* Conjunction.intr_balanced and fold Thm.weaken below, is quadratic for *) (* terms sorted in descending order, while only linear for terms *) (* sorted in ascending order *) - val sorted_clauses = sort (Term_Ord.fast_term_ord o pairself Thm.term_of) nontrivial_clauses + val sorted_clauses = sort (Term_Ord.fast_term_ord o apply2 Thm.term_of) nontrivial_clauses val _ = cond_tracing ctxt (fn () => "Sorted non-trivial clauses:\n" ^ diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/semiring_normalizer.ML --- a/src/HOL/Tools/semiring_normalizer.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/semiring_normalizer.ML Wed Nov 26 20:05:34 2014 +0100 @@ -145,11 +145,11 @@ val cz = rule 34 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg; val cn = rule 36 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg; val ((clx, crx), (cly, cry)) = - rule 13 |> Thm.rhs_of |> Thm.dest_binop |> pairself Thm.dest_binop; + rule 13 |> Thm.rhs_of |> Thm.dest_binop |> apply2 Thm.dest_binop; val ((ca, cb), (cc, cd)) = - rule 20 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_binop; + rule 20 |> Thm.lhs_of |> Thm.dest_binop |> apply2 Thm.dest_binop; val cm = rule 1 |> Thm.rhs_of |> Thm.dest_arg; - val (cp, cq) = rule 26 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_arg; + val (cp, cq) = rule 26 |> Thm.lhs_of |> Thm.dest_binop |> apply2 Thm.dest_arg; val vars = [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry]; val semiring = (sr_ops, sr_rules'); diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/set_comprehension_pointfree.ML --- a/src/HOL/Tools/set_comprehension_pointfree.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/set_comprehension_pointfree.ML Wed Nov 26 20:05:34 2014 +0100 @@ -78,7 +78,7 @@ fun mk_prod1 Ts (t1, t2) = let - val (T1, T2) = pairself (curry fastype_of1 Ts) (t1, t2) + val (T1, T2) = apply2 (curry fastype_of1 Ts) (t1, t2) in HOLogic.pair_const T1 T2 $ t1 $ t2 end; @@ -206,8 +206,8 @@ end; fun map_atoms f (Atom a) = Atom (f a) - | map_atoms f (Un (fm1, fm2)) = Un (pairself (map_atoms f) (fm1, fm2)) - | map_atoms f (Int (fm1, fm2)) = Int (pairself (map_atoms f) (fm1, fm2)) + | map_atoms f (Un (fm1, fm2)) = Un (apply2 (map_atoms f) (fm1, fm2)) + | map_atoms f (Int (fm1, fm2)) = Int (apply2 (map_atoms f) (fm1, fm2)) fun extend Ts bs t = foldr1 mk_sigma (t :: map (fn b => HOLogic.mk_UNIV (nth Ts b)) bs) @@ -237,7 +237,7 @@ fun merge_inter vs (pats1, fm1) (pats2, fm2) = let val pats = restricted_merge (map dest_Pattern pats1, map dest_Pattern pats2) - val (fm1', fm2') = pairself (adjust_atoms vs pats) (fm1, fm2) + val (fm1', fm2') = apply2 (adjust_atoms vs pats) (fm1, fm2) in (map Pattern pats, Int (fm1', fm2')) end; @@ -245,7 +245,7 @@ fun merge_union vs (pats1, fm1) (pats2, fm2) = let val pats = merge (map dest_Pattern pats1, map dest_Pattern pats2) - val (fm1', fm2') = pairself (adjust_atoms vs pats) (fm1, fm2) + val (fm1', fm2') = apply2 (adjust_atoms vs pats) (fm1, fm2) in (map Pattern pats, Un (fm1', fm2')) end; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Tools/try0.ML --- a/src/HOL/Tools/try0.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/try0.ML Wed Nov 26 20:05:34 2014 +0100 @@ -118,7 +118,7 @@ val st = Proof.map_contexts (silence_methods false) st; fun trd (_, _, t) = t; fun par_map f = - if mode = Normal then Par_List.map f #> map_filter I #> sort (int_ord o pairself trd) + if mode = Normal then Par_List.map f #> map_filter I #> sort (int_ord o apply2 trd) else Par_List.get_some f #> the_list; in if mode = Normal then diff -r 5b649fb2f2e1 -r a78612c67ec0 src/HOL/Word/WordBitwise.thy --- a/src/HOL/Word/WordBitwise.thy Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Word/WordBitwise.thy Wed Nov 26 20:05:34 2014 +0100 @@ -510,7 +510,7 @@ case term_of ct of (@{const upt} $ n $ m) => let - val (i, j) = pairself (snd o HOLogic.dest_number) (n, m); + val (i, j) = apply2 (snd o HOLogic.dest_number) (n, m); val ns = map (Numeral.mk_cnumber @{ctyp nat}) (i upto (j - 1)) |> mk_nat_clist; val prop = Thm.mk_binop @{cterm "op = :: nat list => _"} ct ns diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Provers/Arith/fast_lin_arith.ML Wed Nov 26 20:05:34 2014 +0100 @@ -415,7 +415,7 @@ let val c = fold (fn Lineq(_,_,l,_) => fn cs => union (op =) l cs) eqs [] |> filter (fn i => i <> 0) - |> sort (int_ord o pairself abs) + |> sort (int_ord o apply2 abs) |> hd val (eq as Lineq(_,_,ceq,_),othereqs) = extract_first (fn Lineq(_,_,l,_) => member (op =) l c) eqs diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Provers/hypsubst.ML --- a/src/Provers/hypsubst.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Provers/hypsubst.ML Wed Nov 26 20:05:34 2014 +0100 @@ -164,7 +164,7 @@ fun inst_subst_tac ctxt b rl = CSUBGOAL (fn (cBi, i) => case try (Logic.strip_assums_hyp #> hd #> - Data.dest_Trueprop #> Data.dest_eq #> pairself contract) (Thm.term_of cBi) of + Data.dest_Trueprop #> Data.dest_eq #> apply2 contract) (Thm.term_of cBi) of SOME (t, t') => let val thy = Proof_Context.theory_of ctxt; @@ -183,10 +183,10 @@ (case (if b then t else t') of Bound j => subst_bounds (map Bound ((1 upto j) @ 0 :: (j + 2 upto length ps)), Q) | t => Term.abstract_over (t, Term.incr_boundvars 1 Q)); - val (instT, _) = Thm.match (pairself (cterm_of thy o Logic.mk_type) (V, U)); + val (instT, _) = Thm.match (apply2 (cterm_of thy o Logic.mk_type) (V, U)); in compose_tac ctxt (true, Drule.instantiate_normalize (instT, - map (pairself (cterm_of thy)) + map (apply2 (cterm_of thy)) [(Var (ixn, Ts ---> U --> body_type T), u), (Var (fst (dest_Var (head_of v1)), Ts ---> U), fold_rev Term.abs ps t), (Var (fst (dest_Var (head_of v2)), Ts ---> U), fold_rev Term.abs ps t')]) rl', diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Provers/splitter.ML --- a/src/Provers/splitter.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Provers/splitter.ML Wed Nov 26 20:05:34 2014 +0100 @@ -274,7 +274,7 @@ in posns Ts [] [] t end; fun shorter ((_,ps,pos,_,_), (_,qs,qos,_,_)) = - prod_ord (int_ord o pairself length) (order o pairself length) + prod_ord (int_ord o apply2 length) (order o apply2 length) ((ps, pos), (qs, qos)); diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/Concurrent/par_exn.ML --- a/src/Pure/Concurrent/par_exn.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/Concurrent/par_exn.ML Wed Nov 26 20:05:34 2014 +0100 @@ -33,7 +33,7 @@ fun the_serial exn = Markup.parse_int (the (Properties.get (Exn_Properties.get exn) Markup.serialN)); -val exn_ord = rev_order o int_ord o pairself the_serial; +val exn_ord = rev_order o int_ord o apply2 the_serial; (* parallel exceptions *) diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/General/file.ML --- a/src/Pure/General/file.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/General/file.ML Wed Nov 26 20:05:34 2014 +0100 @@ -167,7 +167,7 @@ (* eq *) fun eq paths = - (case try (pairself (OS.FileSys.fileId o platform_path)) paths of + (case try (apply2 (OS.FileSys.fileId o platform_path)) paths of SOME ids => is_equal (OS.FileSys.compare ids) | NONE => false); diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/General/name_space.ML Wed Nov 26 20:05:34 2014 +0100 @@ -152,7 +152,7 @@ NONE => error (undefined kind name) | SOME (_, entry) => entry); -fun entry_ord space = int_ord o pairself (#serial o the_entry space); +fun entry_ord space = int_ord o apply2 (#serial o the_entry space); fun markup (Name_Space {kind, entries, ...}) name = (case Change_Table.lookup entries name of @@ -216,7 +216,7 @@ else ext (get_accesses space name) end; -fun extern_ord ctxt space = string_ord o pairself (extern ctxt space); +fun extern_ord ctxt space = string_ord o apply2 (extern ctxt space); fun extern_shortest ctxt = extern @@ -235,9 +235,9 @@ if Position.is_reported pos andalso xname <> "" andalso xname <> "_" then let fun result_ord ((xname1, (_, name1)), (xname2, (_, name2))) = - (case bool_ord (pairself Long_Name.is_local (name2, name1)) of + (case bool_ord (apply2 Long_Name.is_local (name2, name1)) of EQUAL => - (case int_ord (pairself Long_Name.qualification (xname1, xname2)) of + (case int_ord (apply2 Long_Name.qualification (xname1, xname2)) of EQUAL => string_ord (xname1, xname2) | ord => ord) | ord => ord); @@ -373,7 +373,7 @@ val spec = #2 (name_spec naming binding); val sfxs = mandatory_suffixes spec; val pfxs = mandatory_prefixes spec; - in pairself (map Long_Name.implode) (sfxs @ pfxs, sfxs) end; + in apply2 (map Long_Name.implode) (sfxs @ pfxs, sfxs) end; (* hide *) diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/General/sha1_polyml.ML --- a/src/Pure/General/sha1_polyml.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/General/sha1_polyml.ML Wed Nov 26 20:05:34 2014 +0100 @@ -15,7 +15,7 @@ fun hex_string arr i = let val c = CInterface.fromCchar (CInterface.offset i CInterface.Cchar arr) - in (op ^) (pairself hex_digit (Integer.div_mod (Char.ord c) 16)) end + in (op ^) (apply2 hex_digit (Integer.div_mod (Char.ord c) 16)) end val lib_path = ("$ML_HOME/" ^ (if ML_System.platform_is_cygwin then "sha1.dll" else "libsha1.so")) diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/Isar/calculation.ML --- a/src/Pure/Isar/calculation.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/Isar/calculation.ML Wed Nov 26 20:05:34 2014 +0100 @@ -135,7 +135,7 @@ val pretty_thm_item = Display.pretty_thm_item ctxt; val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of; - val eq_prop = op aconv o pairself (Envir.beta_eta_contract o strip_assums_concl); + val eq_prop = op aconv o apply2 (Envir.beta_eta_contract o strip_assums_concl); fun check_projection ths th = (case find_index (curry eq_prop th) ths of ~1 => Seq.Result [th] diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/Isar/class.ML Wed Nov 26 20:05:34 2014 +0100 @@ -215,7 +215,7 @@ val operations = map (fn (v_ty as (_, ty), (c, _)) => (c, (class, (ty, Free v_ty)))) params; val add_class = Graph.new_node (class, - make_class_data (((map o pairself) fst params, base_sort, + make_class_data (((map o apply2) fst params, base_sort, base_morph, export_morph, some_assm_intro, of_class, some_axiom), ([], operations))) #> fold (curry Graph.add_edge class) sups; in Class_Data.map add_class thy end; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/Isar/code.ML Wed Nov 26 20:05:34 2014 +0100 @@ -655,7 +655,7 @@ val ((abs, raw_ty), ((rep, rep_ty), param)) = (apsnd (apfst dest_Const o dest_comb) o apfst dest_Const o dest_comb) lhs handle TERM _ => bad_thm "Not an abstype certificate"; - val _ = pairself (fn c => if (is_some o Axclass.class_of_param thy) c + val _ = apply2 (fn c => if (is_some o Axclass.class_of_param thy) c then error ("Is a class parameter: " ^ string_of_const thy c) else ()) (abs, rep); val _ = check_decl_ty thy (abs, raw_ty); val _ = check_decl_ty thy (rep, rep_ty); @@ -1035,12 +1035,12 @@ val functions = the_functions exec |> Symtab.dest |> (map o apsnd) (snd o fst) - |> sort (string_ord o pairself fst); + |> sort (string_ord o apply2 fst); val datatypes = the_types exec |> Symtab.dest |> map (fn (tyco, (_, (vs, spec)) :: _) => ((tyco, vs), constructors_of spec)) - |> sort (string_ord o pairself (fst o fst)); + |> sort (string_ord o apply2 (fst o fst)); val cases = Symtab.dest ((fst o the_cases o the_exec) thy); val undefineds = Symtab.keys ((snd o the_cases o the_exec) thy); in @@ -1171,7 +1171,7 @@ val T_cong = nth Ts pos; fun mk_prem z = Free (z, T_cong); fun mk_concl z = list_comb (Const (case_const, T), map2 (curry Free) (ws @ z :: vs) Ts); - val (prem, concl) = pairself Logic.mk_equals (pairself mk_prem (x, y), pairself mk_concl (x, y)); + val (prem, concl) = apply2 Logic.mk_equals (apply2 mk_prem (x, y), apply2 mk_concl (x, y)); in Goal.prove_sorry_global thy (x :: y :: zs) [prem] concl (fn {context = ctxt', prems} => diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/Isar/context_rules.ML --- a/src/Pure/Isar/context_rules.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/Isar/context_rules.ML Wed Nov 26 20:05:34 2014 +0100 @@ -119,7 +119,7 @@ Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":") (map_filter (fn (_, (k, th)) => if k = (i, b) then SOME (Display.pretty_thm_item ctxt th) else NONE) - (sort (int_ord o pairself fst) rules)); + (sort (int_ord o apply2 fst) rules)); in Pretty.writeln_chunks (map prt_kind rule_kinds) end; @@ -139,10 +139,10 @@ else x :: untaglist rest; fun orderlist brls = - untaglist (sort (prod_ord int_ord int_ord o pairself fst) brls); + untaglist (sort (prod_ord int_ord int_ord o apply2 fst) brls); fun orderlist_no_weight brls = - untaglist (sort (int_ord o pairself (snd o fst)) brls); + untaglist (sort (int_ord o apply2 (snd o fst)) brls); fun may_unify weighted t net = map snd ((if weighted then orderlist else orderlist_no_weight) (Net.unify_term net t)); diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/Isar/generic_target.ML --- a/src/Pure/Isar/generic_target.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/Isar/generic_target.ML Wed Nov 26 20:05:34 2014 +0100 @@ -167,7 +167,7 @@ fun background_abbrev (b, global_rhs) params = Local_Theory.background_theory_result (Sign.add_abbrev Print_Mode.internal (b, global_rhs)) - #>> pairself (fn t => Term.list_comb (Logic.unvarify_global t, params)) + #>> apply2 (fn t => Term.list_comb (Logic.unvarify_global t, params)) (** lifting primitive to local theory operations **) @@ -190,7 +190,7 @@ val mx' = check_mixfix lthy (b, extra_tfrees) mx; val type_params = map (Logic.mk_type o TFree) extra_tfrees; - val term_params = map Free (sort (Variable.fixed_ord lthy o pairself #1) xs); + val term_params = map Free (sort (Variable.fixed_ord lthy o apply2 #1) xs); val params = type_params @ term_params; val U = map Term.fastype_of params ---> T; @@ -247,8 +247,8 @@ val instT = map_filter (fn (TVar v, T) => SOME (v, T) | _ => NONE) (tvars ~~ tfrees); val inst = filter (is_Var o fst) (vars ~~ frees); - val cinstT = map (pairself certT o apfst TVar) instT; - val cinst = map (pairself (cert o Term.map_types (Term_Subst.instantiateT instT))) inst; + val cinstT = map (apply2 certT o apfst TVar) instT; + val cinst = map (apply2 (cert o Term.map_types (Term_Subst.instantiateT instT))) inst; val result' = Thm.instantiate (cinstT, cinst) result; (*import assumes/defines*) @@ -287,7 +287,7 @@ val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy); val rhs' = Assumption.export_term lthy (Local_Theory.target_of lthy) rhs; - val term_params = map Free (sort (Variable.fixed_ord lthy o pairself #1) (Variable.add_fixed lthy rhs' [])); + val term_params = map Free (sort (Variable.fixed_ord lthy o apply2 #1) (Variable.add_fixed lthy rhs' [])); val u = fold_rev lambda term_params rhs'; val global_rhs = singleton (Variable.polymorphic thy_ctxt) u; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/Isar/local_defs.ML --- a/src/Pure/Isar/local_defs.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/Isar/local_defs.ML Wed Nov 26 20:05:34 2014 +0100 @@ -149,7 +149,7 @@ if t aconv u then (asm, false) else (Drule.abs_def (Drule.gen_all asm), true)) end))); - in (pairself (map #1) (List.partition #2 defs_asms), th') end + in (apply2 (map #1) (List.partition #2 defs_asms), th') end end; (* diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/Isar/proof_context.ML Wed Nov 26 20:05:34 2014 +0100 @@ -1176,7 +1176,7 @@ fun dest_cases ctxt = Name_Space.fold_table (fn (a, (c, i)) => cons (i, (a, c))) (cases_of ctxt) [] - |> sort (int_ord o pairself #1) |> map #2; + |> sort (int_ord o apply2 #1) |> map #2; local @@ -1255,7 +1255,7 @@ let val space = const_space ctxt; val (constants, global_constants) = - pairself (#constants o Consts.dest) (#consts (rep_data ctxt)); + apply2 (#constants o Consts.dest) (#consts (rep_data ctxt)); val globals = Symtab.make global_constants; fun add_abbr (_, (_, NONE)) = I | add_abbr (c, (T, SOME t)) = diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/Isar/rule_cases.ML --- a/src/Pure/Isar/rule_cases.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/Isar/rule_cases.ML Wed Nov 26 20:05:34 2014 +0100 @@ -123,7 +123,7 @@ (app (map (Term.dummy_pattern o #2) fixes2) (fold_rev Term.abs fixes2 t)); val (assumes1, assumes2) = extract_assumes name hyp_names case_outline prop - |> pairself (map (apsnd (maps Logic.dest_conjunctions))); + |> apply2 (map (apsnd (maps Logic.dest_conjunctions))); val concl = Object_Logic.drop_judgment thy (Logic.strip_assums_concl prop); val binds = @@ -428,7 +428,7 @@ local fun equal_cterms ts us = - is_equal (list_ord (Term_Ord.fast_term_ord o pairself Thm.term_of) (ts, us)); + is_equal (list_ord (Term_Ord.fast_term_ord o apply2 Thm.term_of) (ts, us)); fun prep_rule n th = let diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/Isar/runtime.ML --- a/src/Pure/Isar/runtime.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/Isar/runtime.ML Wed Nov 26 20:05:34 2014 +0100 @@ -119,7 +119,7 @@ | _ => raised exn (robust (Pretty.string_of o Exn_Output.pretty) exn) []); in [((i, msg), id)] end) and sorted_msgs context exn = - sort_distinct (int_ord o pairself (fst o fst)) (maps exn_msgs (flatten context exn)); + sort_distinct (int_ord o apply2 (fst o fst)) (maps exn_msgs (flatten context exn)); in sorted_msgs NONE e end; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/ML/ml_context.ML --- a/src/Pure/ML/ml_context.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/ML/ml_context.ML Wed Nov 26 20:05:34 2014 +0100 @@ -124,7 +124,7 @@ val keywords = Thy_Header.get_keywords' ctxt; val (decl, ctxt') = apply_antiquotation (Token.read_antiq keywords antiq (ss, #1 range)) ctxt; - val decl' = decl #> pairself (ML_Lex.tokenize #> map (ML_Lex.set_range range)); + val decl' = decl #> apply2 (ML_Lex.tokenize #> map (ML_Lex.set_range range)); in (decl', ctxt') end; val ctxt = @@ -134,7 +134,7 @@ val (decls, ctxt') = fold_map expand ants ctxt; val (ml_env, ml_body) = - decls |> map (fn decl => decl ctxt') |> split_list |> pairself flat; + decls |> map (fn decl => decl ctxt') |> split_list |> apply2 flat; in ((begin_env visible @ ml_env, ml_body), SOME (Context.Proof ctxt')) end; in ((ml_env @ end_env, ml_body), opt_ctxt') end; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/ML/ml_env.ML --- a/src/Pure/ML/ml_env.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/ML/ml_env.ML Wed Nov 26 20:05:34 2014 +0100 @@ -57,8 +57,8 @@ fun extend (data : T) = make_data (false, #tables data, #sml_tables data); fun merge (data : T * T) = make_data (false, - merge_tables (pairself #tables data), - merge_tables (pairself #sml_tables data)); + merge_tables (apply2 #tables data), + merge_tables (apply2 #sml_tables data)); ); val inherit = Env.put o Env.get; @@ -85,7 +85,7 @@ Context.thread_data () |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#tables (Env.get context)))) |> append (sel2 ML_Name_Space.global ())) - |> sort_distinct (string_ord o pairself #1); + |> sort_distinct (string_ord o apply2 #1); fun enter ap1 sel2 entry = if SML <> exchange then diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/PIDE/command.ML Wed Nov 26 20:05:34 2014 +0100 @@ -187,7 +187,7 @@ datatype eval = Eval of {exec_id: Document_ID.exec, eval_process: eval_state memo}; fun eval_exec_id (Eval {exec_id, ...}) = exec_id; -val eval_eq = op = o pairself eval_exec_id; +val eval_eq = op = o apply2 eval_exec_id; val eval_running = Execution.is_running_exec o eval_exec_id; fun eval_finished (Eval {eval_process, ...}) = memo_finished eval_process; @@ -291,7 +291,7 @@ exec_id: Document_ID.exec, print_process: unit memo}; fun print_exec_id (Print {exec_id, ...}) = exec_id; -val print_eq = op = o pairself print_exec_id; +val print_eq = op = o apply2 print_exec_id; type print_fn = Toplevel.transition -> Toplevel.state -> unit; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/Proof/extraction.ML Wed Nov 26 20:05:34 2014 +0100 @@ -103,14 +103,14 @@ fun ren t = the_default t (Term.rename_abs tm1 tm t); val inc = Logic.incr_indexes ([], maxidx_of_term tm + 1); val env as (Tenv, tenv) = Pattern.match thy (inc tm1, tm) (Vartab.empty, Vartab.empty); - val prems' = map (pairself (Envir.subst_term env o inc o ren)) prems; + val prems' = map (apply2 (Envir.subst_term env o inc o ren)) prems; val env' = Envir.Envir {maxidx = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u) prems' ~1, tenv = tenv, tyenv = Tenv}; - val env'' = fold (Pattern.unify (Context.Theory thy) o pairself (lookup rew)) prems' env'; + val env'' = fold (Pattern.unify (Context.Theory thy) o apply2 (lookup rew)) prems' env'; in SOME (Envir.norm_term env'' (inc (ren tm2))) end handle Pattern.MATCH => NONE | Pattern.Unif => NONE) - (sort (int_ord o pairself fst) + (sort (int_ord o apply2 fst) (Net.match_term rules (Envir.eta_contract tm))) end; @@ -207,7 +207,7 @@ {realizes_eqns = merge_rules realizes_eqns1 realizes_eqns2, typeof_eqns = merge_rules typeof_eqns1 typeof_eqns2, types = AList.merge (op =) (K true) (types1, types2), - realizers = Symtab.merge_list (eq_set (op =) o pairself #1) (realizers1, realizers2), + realizers = Symtab.merge_list (eq_set (op =) o apply2 #1) (realizers1, realizers2), defs = Library.merge Thm.eq_thm (defs1, defs2), expand = Library.merge (op =) (expand1, expand2), prep = if is_some prep1 then prep1 else prep2}; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/Proof/proof_checker.ML --- a/src/Pure/Proof/proof_checker.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/Proof/proof_checker.ML Wed Nov 26 20:05:34 2014 +0100 @@ -78,7 +78,7 @@ let val tvars = Term.add_tvars (Thm.full_prop_of thm) [] |> rev; val (fmap, thm') = Thm.varifyT_global' [] thm; - val ctye = map (pairself (Thm.ctyp_of thy)) + val ctye = map (apply2 (Thm.ctyp_of thy)) (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts) in Thm.instantiate (ctye, []) (forall_intr_vars (Thm.forall_intr_frees thm')) diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/Proof/reconstruct.ML --- a/src/Pure/Proof/reconstruct.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/Proof/reconstruct.ML Wed Nov 26 20:05:34 2014 +0100 @@ -100,7 +100,7 @@ if a <> b then cantunify thy p else apfst flat (fold_map (decompose thy Ts) (ts ~~ us) (uT env T U)) in - case pairself (strip_comb o Envir.head_norm env) p of + case apply2 (strip_comb o Envir.head_norm env) p of ((Const c, ts), (Const d, us)) => rigrig c d (unifyT thy) ts us | ((Free c, ts), (Free d, us)) => rigrig c d (unifyT thy) ts us | ((Bound i, ts), (Bound j, us)) => @@ -254,7 +254,7 @@ let fun search env [] = error ("Unsolvable constraints:\n" ^ Pretty.string_of (Pretty.chunks (map (fn (_, p, _) => - Goal_Display.pretty_flexpair (Syntax.init_pretty_global thy) (pairself + Goal_Display.pretty_flexpair (Syntax.init_pretty_global thy) (apply2 (Envir.norm_term bigenv) p)) cs))) | search env ((u, p as (t1, t2), vs)::ps) = if u then @@ -289,7 +289,7 @@ val (t, prf, cs, env, _) = make_constraints_cprf thy (Envir.empty (Proofterm.maxidx_proof cprf ~1)) cprf'; val cs' = - map (pairself (Envir.norm_term env)) ((t, prop') :: cs) + map (apply2 (Envir.norm_term env)) ((t, prop') :: cs) |> map (fn p => (true, p, Term.add_var_names (#1 p) (Term.add_var_names (#2 p) []))); val _ = message ("Solving remaining constraints (" ^ string_of_int (length cs') ^ ") ..."); val env' = solve thy cs' env diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/Syntax/syntax_phases.ML Wed Nov 26 20:05:34 2014 +0100 @@ -864,8 +864,8 @@ let fun split_checks checks = List.partition (fn ((_, un), _) => not un) checks - |> pairself (map (fn ((i, _), fs) => (i, map (fst o fst) fs)) - #> sort (int_ord o pairself fst)); + |> apply2 (map (fn ((i, _), fs) => (i, map (fst o fst) fs)) + #> sort (int_ord o apply2 fst)); fun pretty_checks kind checks = checks |> map (fn (i, names) => Pretty.block [Pretty.str (kind ^ " (stage " ^ signed_string_of_int i ^ "):"), @@ -915,7 +915,7 @@ let val funs = which (Checks.get (Context.Proof ctxt0)) |> map_filter (fn ((i, u), fs) => if uncheck = u then SOME (i, map (snd o fst) fs) else NONE) - |> Library.sort (int_ord o pairself fst) |> map snd + |> Library.sort (int_ord o apply2 fst) |> map snd |> not uncheck ? map rev; in #1 (perhaps (check_all funs) (xs0, ctxt0)) end; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/System/message_channel.ML --- a/src/Pure/System/message_channel.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/System/message_channel.ML Wed Nov 26 20:05:34 2014 +0100 @@ -26,7 +26,7 @@ fun message name raw_props body = let - val robust_props = map (pairself YXML.embed_controls) raw_props; + val robust_props = map (apply2 YXML.embed_controls) raw_props; val header = YXML.string_of (XML.Elem ((name, robust_props), [])); in Message (chunk [header] @ chunk body) end; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/Thy/present.ML Wed Nov 26 20:05:34 2014 +0100 @@ -277,7 +277,7 @@ (* finish session -- output all generated text *) -fun sorted_index index = map snd (sort (int_ord o pairself fst) (rev index)); +fun sorted_index index = map snd (sort (int_ord o apply2 fst) (rev index)); fun index_buffer index = Buffer.add (implode (sorted_index index)) Buffer.empty; fun write_tex src name path = diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/Tools/build.ML Wed Nov 26 20:05:34 2014 +0100 @@ -147,7 +147,7 @@ (Options.bool options "document_graph") (Options.string options "document_output") (Present.document_variants (Options.string options "document_variants")) - (map (pairself Path.explode) document_files) + (map (apply2 Path.explode) document_files) parent_name (chapter, name) verbose; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/Tools/class_deps.ML --- a/src/Pure/Tools/class_deps.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/Tools/class_deps.ML Wed Nov 26 20:05:34 2014 +0100 @@ -30,7 +30,7 @@ dir = "", unfold = true, path = "", content = []}); val gr = Graph.fold (cons o entry) classes [] - |> sort (int_ord o pairself #1) |> map #2; + |> sort (int_ord o apply2 #1) |> map #2; in Graph_Display.display_graph gr end; val visualize = gen_visualize (Type.cert_sort o Proof_Context.tsig_of); diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/Tools/find_consts.ML --- a/src/Pure/Tools/find_consts.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/Tools/find_consts.ML Wed Nov 26 20:05:34 2014 +0100 @@ -110,7 +110,7 @@ val matches = fold (fn c => (case eval_entry c of NONE => I | SOME rank => cons (rank, c))) constants [] - |> sort (prod_ord (rev_order o int_ord) (string_ord o pairself fst)) + |> sort (prod_ord (rev_order o int_ord) (string_ord o apply2 fst)) |> map (apsnd fst o snd); val position_markup = Position.markup (Position.thread_data ()) Markup.position; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/Tools/find_theorems.ML Wed Nov 26 20:05:34 2014 +0100 @@ -330,9 +330,9 @@ local val index_ord = option_ord (K EQUAL); -val hidden_ord = bool_ord o pairself Long_Name.is_hidden; -val qual_ord = int_ord o pairself Long_Name.qualification; -val txt_ord = int_ord o pairself size; +val hidden_ord = bool_ord o apply2 Long_Name.is_hidden; +val qual_ord = int_ord o apply2 Long_Name.qualification; +val txt_ord = int_ord o apply2 size; fun nicer_name (x, i) (y, j) = (case hidden_ord (x, y) of EQUAL => @@ -368,9 +368,9 @@ fun rem_thm_dups nicer xs = (xs ~~ (1 upto length xs)) - |> sort (Term_Ord.fast_term_ord o pairself (Thm.full_prop_of o #2 o #1)) + |> sort (Term_Ord.fast_term_ord o apply2 (Thm.full_prop_of o #2 o #1)) |> rem_cdups nicer - |> sort (int_ord o pairself #2) + |> sort (int_ord o apply2 #2) |> map #1; end; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/Tools/plugin.ML --- a/src/Pure/Tools/plugin.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/Tools/plugin.ML Wed Nov 26 20:05:34 2014 +0100 @@ -112,8 +112,8 @@ type data = {filter: Plugin_Name.filter, naming: Name_Space.naming, value: T, id: serial}; type interp = {name: string, apply: T -> local_theory -> local_theory, id: serial}; -val eq_data: data * data -> bool = op = o pairself #id; -val eq_interp: interp * interp -> bool = op = o pairself #id; +val eq_data: data * data -> bool = op = o apply2 #id; +val eq_interp: interp * interp -> bool = op = o apply2 #id; fun mk_data filter naming x : data = {filter = filter, naming = naming, value = x, id = serial ()}; fun mk_interp name f : interp = {name = name, apply = f, id = serial ()}; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/Tools/rail.ML --- a/src/Pure/Tools/rail.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/Tools/rail.ML Wed Nov 26 20:05:34 2014 +0100 @@ -265,11 +265,11 @@ fun prepare_trees (CAT (ts, _)) = Cat (0, map prepare_tree ts) and prepare_tree (BAR (Ts, _)) = bar (map prepare_trees Ts) | prepare_tree (STAR (Ts, _)) = - let val (cat1, cat2) = pairself prepare_trees Ts in + let val (cat1, cat2) = apply2 prepare_trees Ts in if is_empty cat2 then plus (empty, cat1) else bar [empty, cat [plus (cat1, cat2)]] end - | prepare_tree (PLUS (Ts, _)) = plus (pairself prepare_trees Ts) + | prepare_tree (PLUS (Ts, _)) = plus (apply2 prepare_trees Ts) | prepare_tree (MAYBE (t, _)) = bar [empty, cat [prepare_tree t]] | prepare_tree (NEWLINE _) = Newline 0 | prepare_tree (NONTERMINAL (a, _)) = Nonterminal a diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/Tools/rule_insts.ML --- a/src/Pure/Tools/rule_insts.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/Tools/rule_insts.ML Wed Nov 26 20:05:34 2014 +0100 @@ -118,7 +118,7 @@ val inst_tvars = map_filter (make_instT (instT2 o instT1)) tvars; val inst_vars = map_filter (make_inst inst2) vars2; in - (map (pairself certT) inst_tvars, map (pairself cert) inst_vars) + (map (apply2 certT) inst_tvars, map (apply2 cert) inst_vars) end; fun where_rule ctxt mixed_insts fixes thm = @@ -251,7 +251,7 @@ val cenv = map (fn (xi, t) => - pairself (Thm.cterm_of thy) (Var (xi, fastype_of t), t)) + apply2 (Thm.cterm_of thy) (Var (xi, fastype_of t), t)) (distinct (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2) (xis ~~ ts)); @@ -265,7 +265,7 @@ fun liftterm t = fold_rev absfree (param_names ~~ paramTs) (Logic.incr_indexes (paramTs, inc) t); fun liftpair (cv, ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct); - val lifttvar = pairself (ctyp_of thy o Logic.incr_tvar inc); + val lifttvar = apply2 (ctyp_of thy o Logic.incr_tvar inc); val rule = Drule.instantiate_normalize (map lifttvar envT', map liftpair cenv) (Thm.lift_rule cgoal thm) diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/Tools/thm_deps.ML --- a/src/Pure/Tools/thm_deps.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/Tools/thm_deps.ML Wed Nov 26 20:05:34 2014 +0100 @@ -68,7 +68,7 @@ val new_thms = fold (add_facts o Global_Theory.facts_of) thys [] - |> sort_distinct (string_ord o pairself #1); + |> sort_distinct (string_ord o apply2 #1); val used = Proofterm.fold_body_thms diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/axclass.ML --- a/src/Pure/axclass.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/axclass.ML Wed Nov 26 20:05:34 2014 +0100 @@ -321,7 +321,7 @@ fun cert_classrel thy raw_rel = let val string_of_sort = Syntax.string_of_sort_global thy; - val (c1, c2) = pairself (Sign.certify_class thy) raw_rel; + val (c1, c2) = apply2 (Sign.certify_class thy) raw_rel; val _ = Sign.primitive_classrel (c1, c2) thy; val _ = (case subtract (op =) (all_params_of thy [c1]) (all_params_of thy [c2]) of @@ -331,7 +331,7 @@ in (c1, c2) end; fun read_classrel thy raw_rel = - cert_classrel thy (pairself (Proof_Context.read_class (Proof_Context.init_global thy)) raw_rel) + cert_classrel thy (apply2 (Proof_Context.read_class (Proof_Context.init_global thy)) raw_rel) handle TYPE (msg, _, _) => error msg; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/context.ML --- a/src/Pure/context.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/context.ML Wed Nov 26 20:05:34 2014 +0100 @@ -145,7 +145,7 @@ in k end; val extend_data = Datatab.map invoke_extend; -fun merge_data pp = Datatab.join (invoke_merge pp) o pairself extend_data; +fun merge_data pp = Datatab.join (invoke_merge pp) o apply2 extend_data; end; @@ -238,7 +238,7 @@ (* equality and inclusion *) -val eq_thy = op = o pairself (#id o identity_of); +val eq_thy = op = o apply2 (#id o identity_of); fun proper_subthy (Theory ({id, ...}, _, _, _), Theory ({ids, ...}, _, _, _)) = Inttab.defined ids id; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/drule.ML --- a/src/Pure/drule.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/drule.ML Wed Nov 26 20:05:34 2014 +0100 @@ -797,7 +797,7 @@ val instT = Vartab.fold (fn (xi, (S, T)) => cons (certT (TVar (xi, S)), certT (Envir.norm_type tye T))) tye []; - val inst = map (pairself (Thm.instantiate_cterm (instT, []))) ctpairs; + val inst = map (apply2 (Thm.instantiate_cterm (instT, []))) ctpairs; in instantiate_normalize (instT, inst) th end handle TERM (msg, _) => raise THM (msg, 0, [th]) | TYPE (msg, _, _) => raise THM (msg, 0, [th]); diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/facts.ML --- a/src/Pure/facts.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/facts.ML Wed Nov 26 20:05:34 2014 +0100 @@ -206,7 +206,7 @@ (* indexed props *) -val prop_ord = Term_Ord.term_ord o pairself Thm.full_prop_of; +val prop_ord = Term_Ord.term_ord o apply2 Thm.full_prop_of; fun props (Facts {props, ...}) = sort_distinct prop_ord (Net.content props); fun could_unify (Facts {props, ...}) = Net.unify_term props; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/item_net.ML --- a/src/Pure/item_net.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/item_net.ML Wed Nov 26 20:05:34 2014 +0100 @@ -64,7 +64,7 @@ fun remove x (items as Items {eq, index, content, next, net}) = if member items x then mk_items eq index (Library.remove eq x content) next - (fold (fn t => Net.delete_term_safe (eq o pairself #2) (t, (0, x))) (index x) net) + (fold (fn t => Net.delete_term_safe (eq o apply2 #2) (t, (0, x))) (index x) net) else items; fun update x items = cons x (remove x items); diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/library.ML --- a/src/Pure/library.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/library.ML Wed Nov 26 20:05:34 2014 +0100 @@ -44,7 +44,7 @@ val swap: 'a * 'b -> 'b * 'a val apfst: ('a -> 'b) -> 'a * 'c -> 'b * 'c val apsnd: ('a -> 'b) -> 'c * 'a -> 'c * 'b - val pairself: ('a -> 'b) -> 'a * 'a -> 'b * 'b + val apply2: ('a -> 'b) -> 'a * 'a -> 'b * 'b (*booleans*) val equal: ''a -> ''a -> bool @@ -283,7 +283,7 @@ fun apfst f (x, y) = (f x, y); fun apsnd f (x, y) = (x, f y); -fun pairself f (x, y) = (f x, f y); +fun apply2 f (x, y) = (f x, f y); (* booleans *) @@ -964,7 +964,7 @@ fun sort_distinct ord = mergesort true ord; val sort_strings = sort string_ord; -fun sort_wrt key xs = sort (string_ord o pairself key) xs; +fun sort_wrt key xs = sort (string_ord o apply2 key) xs; (* items tagged by integer index *) @@ -981,7 +981,7 @@ else x :: untag_list rest; (*return list elements in original order*) -fun order_list list = untag_list (sort (int_ord o pairself fst) list); +fun order_list list = untag_list (sort (int_ord o apply2 fst) list); diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/more_thm.ML Wed Nov 26 20:05:34 2014 +0100 @@ -112,7 +112,7 @@ (* collecting cterms *) -val op aconvc = op aconv o pairself Thm.term_of; +val op aconvc = op aconv o apply2 Thm.term_of; fun add_cterm_frees ct = let @@ -179,7 +179,7 @@ (* tables and caches *) -structure Ctermtab = Table(type key = cterm val ord = Term_Ord.fast_term_ord o pairself Thm.term_of); +structure Ctermtab = Table(type key = cterm val ord = Term_Ord.fast_term_ord o apply2 Thm.term_of); structure Thmtab = Table(type key = thm val ord = thm_ord); fun cterm_cache f = Cache.create Ctermtab.empty Ctermtab.lookup Ctermtab.update f; @@ -193,11 +193,11 @@ val eq_thm = is_equal o thm_ord; -val eq_thm_prop = op aconv o pairself Thm.full_prop_of; +val eq_thm_prop = op aconv o apply2 Thm.full_prop_of; fun eq_thm_strict ths = eq_thm ths andalso - let val (rep1, rep2) = pairself Thm.rep_thm ths in + let val (rep1, rep2) = apply2 Thm.rep_thm ths in Theory.eq_thy (#thy rep1, #thy rep2) andalso #maxidx rep1 = #maxidx rep2 andalso #tags rep1 = #tags rep2 @@ -207,7 +207,7 @@ (* pattern equivalence *) fun equiv_thm ths = - Pattern.equiv (Theory.merge (pairself Thm.theory_of_thm ths)) (pairself Thm.full_prop_of ths); + Pattern.equiv (Theory.merge (apply2 Thm.theory_of_thm ths)) (apply2 Thm.full_prop_of ths); (* type classes and sorts *) @@ -397,7 +397,7 @@ val tfrees = rev (map TFree (Term.add_tfrees t [])); val tfrees' = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT (length tfrees)); val strip = tfrees ~~ tfrees'; - val recover = map (pairself (Thm.ctyp_of thy o Logic.varifyT_global) o swap) strip; + val recover = map (apply2 (Thm.ctyp_of thy o Logic.varifyT_global) o swap) strip; val t' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip))) t; in (strip, recover, t') end; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/proofterm.ML Wed Nov 26 20:05:34 2014 +0100 @@ -1226,7 +1226,7 @@ | (f $ t, g $ u) => mtch (mtch instsp (f, g)) (t, u) | (Bound i, Bound j) => if i=j then instsp else raise PMatch | _ => raise PMatch - in mtch instsp (pairself Envir.beta_eta_contract p) end; + in mtch instsp (apply2 Envir.beta_eta_contract p) end; fun match_proof Ts tymatch = let diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/raw_simplifier.ML Wed Nov 26 20:05:34 2014 +0100 @@ -342,7 +342,7 @@ val rules' = Net.merge eq_rrule (rules1, rules2); val prems' = Thm.merge_thms (prems1, prems2); val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1; - val congs' = merge (Thm.eq_thm_prop o pairself #2) (congs1, congs2); + val congs' = merge (Thm.eq_thm_prop o apply2 #2) (congs1, congs2); val weak' = merge (op =) (weak1, weak2); val procs' = Net.merge eq_proc (procs1, procs2); val loop_tacs' = AList.merge (op =) (K true) (loop_tacs1, loop_tacs2); @@ -1036,7 +1036,7 @@ (case check_conv ctxt true (Drule.beta_eta_conversion t) thm2 of NONE => err ("Congruence proof failed. Should not have proved", thm2) | SOME thm2' => - if op aconv (pairself term_of (Thm.dest_equals (cprop_of thm2'))) + if op aconv (apply2 term_of (Thm.dest_equals (cprop_of thm2'))) then NONE else SOME thm2')) end; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/search.ML --- a/src/Pure/search.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/search.ML Wed Nov 26 20:05:34 2014 +0100 @@ -194,7 +194,7 @@ structure Thm_Heap = Heap ( type elem = int * thm; - val ord = prod_ord int_ord (Term_Ord.term_ord o pairself Thm.prop_of); + val ord = prod_ord int_ord (Term_Ord.term_ord o apply2 Thm.prop_of); ); val trace_BEST_FIRST = Unsynchronized.ref false; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/subgoal.ML --- a/src/Pure/subgoal.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/subgoal.ML Wed Nov 26 20:05:34 2014 +0100 @@ -86,7 +86,7 @@ else (Ts ---> T, ts); val u = Free (y, U); in ((Var v, list_comb (u, args)), (u, Var ((x, i + idx), U))) end; - val (inst1, inst2) = split_list (map (pairself (pairself cert)) (map2 var_inst vars ys)); + val (inst1, inst2) = split_list (map (apply2 (apply2 cert)) (map2 var_inst vars ys)); val th'' = Thm.instantiate ([], inst1) th'; in ((inst2, th''), ctxt'') end; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/thm.ML --- a/src/Pure/thm.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/thm.ML Wed Nov 26 20:05:34 2014 +0100 @@ -338,7 +338,7 @@ let fun cterm max t = Cterm {thy = thy, t = t, T = propT, maxidx = max, sorts = shyps} in {thy = thy, tags = tags, maxidx = maxidx, shyps = shyps, hyps = map (cterm ~1) hyps, - tpairs = map (pairself (cterm maxidx)) tpairs, + tpairs = map (apply2 (cterm maxidx)) tpairs, prop = cterm maxidx prop} end; @@ -1000,7 +1000,7 @@ if Envir.is_empty env then th else let - val tpairs' = tpairs |> map (pairself (Envir.norm_term env)) + val tpairs' = tpairs |> map (apply2 (Envir.norm_term env)) (*remove trivial tpairs, of the form t==t*) |> filter_out (op aconv); val der' = deriv_rule1 (Proofterm.norm_proof' env) der; @@ -1039,7 +1039,7 @@ val gen = Term_Subst.generalize (tfrees, frees) idx; val prop' = gen prop; - val tpairs' = map (pairself gen) tpairs; + val tpairs' = map (apply2 gen) tpairs; val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop'); in Thm (deriv_rule1 (Proofterm.generalize (tfrees, frees) idx) der, @@ -1291,7 +1291,7 @@ maxidx = maxidx + inc, shyps = Sorts.union shyps sorts, (*sic!*) hyps = hyps, - tpairs = map (pairself lift_abs) tpairs, + tpairs = map (apply2 lift_abs) tpairs, prop = Logic.list_implies (map lift_all As, lift_all B)}) end; @@ -1305,7 +1305,7 @@ maxidx = maxidx + i, shyps = shyps, hyps = hyps, - tpairs = map (pairself (Logic.incr_indexes ([], i))) tpairs, + tpairs = map (apply2 (Logic.incr_indexes ([], i))) tpairs, prop = Logic.incr_indexes ([], i) prop}); (*Solve subgoal Bi of proof state B1...Bn/C by assumption. *) @@ -1324,7 +1324,7 @@ hyps = hyps, tpairs = if Envir.is_empty env then tpairs - else map (pairself (Envir.norm_term env)) tpairs, + else map (apply2 (Envir.norm_term env)) tpairs, prop = if Envir.is_empty env then (*avoid wasted normalizations*) Logic.list_implies (Bs, C) @@ -1504,7 +1504,7 @@ |> fold (add_var o snd) tpairs; val vids' = fold (add_var o strip_lifted B) As []; (*unknowns appearing elsewhere be preserved!*) - val al' = distinct ((op =) o pairself fst) + val al' = distinct ((op =) o apply2 fst) (filter_out (fn (x, y) => not (member (op =) vids' x) orelse member (op =) vids x orelse member (op =) vids y) al); @@ -1598,7 +1598,7 @@ val (ntpairs, normp) = if Envir.is_empty env then (tpairs, (Bs @ As, C)) else - let val ntps = map (pairself normt) tpairs + let val ntps = map (apply2 normt) tpairs in if Envir.above env smax then (*no assignments in state; normalize the rule only*) if lifted diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/type.ML --- a/src/Pure/type.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/type.ML Wed Nov 26 20:05:34 2014 +0100 @@ -188,7 +188,7 @@ let val log_types = Name_Space.fold_table (fn (c, LogicalType n) => cons (c, n) | _ => I) types [] - |> Library.sort (int_ord o pairself snd) |> map fst; + |> Library.sort (int_ord o apply2 snd) |> map fst; in make_tsig (classes, default, types, log_types) end; fun map_tsig f (TSig {classes, default, types, log_types = _}) = @@ -639,7 +639,7 @@ fun add_classrel pp rel tsig = tsig |> map_tsig (fn ((space, classes), default, types) => let - val rel' = pairself (cert_class tsig) rel + val rel' = apply2 (cert_class tsig) rel handle TYPE (msg, _, _) => error msg; val classes' = classes |> Sorts.add_classrel pp rel'; in ((space, classes'), default, types) end); diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/type_infer_context.ML --- a/src/Pure/type_infer_context.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/type_infer_context.ML Wed Nov 26 20:05:34 2014 +0100 @@ -219,7 +219,7 @@ quote (Syntax.string_of_typ ctxt (Type (a, replicate (length Ts) dummyT))); fun unif (T1, T2) (env as (tye, _)) = - (case pairself (`Type_Infer.is_paramT o Type_Infer.deref tye) (T1, T2) of + (case apply2 (`Type_Infer.is_paramT o Type_Infer.deref tye) (T1, T2) of ((true, TVar (xi, S)), (_, T)) => assign xi T S env | ((_, T), (true, TVar (xi, S))) => assign xi T S env | ((_, Type (a, Ts)), (_, Type (b, Us))) => diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/variable.ML --- a/src/Pure/variable.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Pure/variable.ML Wed Nov 26 20:05:34 2014 +0100 @@ -352,7 +352,7 @@ fun dest_fixes ctxt = Name_Space.fold_table (fn (x, y) => cons (y, x)) (fixes_of ctxt) [] - |> sort (Name_Space.entry_ord (fixes_space ctxt) o pairself #2); + |> sort (Name_Space.entry_ord (fixes_space ctxt) o apply2 #2); (* collect variables *) @@ -403,7 +403,7 @@ [] => () | bads => error ("Illegal internal Skolem constant(s): " ^ commas (map Binding.print bads))); val _ = - (case duplicates (op = o pairself Binding.name_of) bs of + (case duplicates (op = o apply2 Binding.name_of) bs of [] => () | dups => err_dups dups); diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Tools/Code/code_namespace.ML --- a/src/Tools/Code/code_namespace.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Tools/Code/code_namespace.ML Wed Nov 26 20:05:34 2014 +0100 @@ -384,7 +384,7 @@ val (name_fragments_common, (diff, diff')) = chop_prefix (op =) (name_fragments, name_fragments'); val is_cross_module = not (null diff andalso null diff'); - val dep = pairself hd (map Code_Symbol.Module diff @ [sym], map Code_Symbol.Module diff' @ [sym']); + val dep = apply2 hd (map Code_Symbol.Module diff @ [sym], map Code_Symbol.Module diff' @ [sym']); val add_edge = if is_cross_module andalso not cyclic_modules then add_edge_acyclic_error (fn _ => "Dependency " ^ Code_Symbol.quote ctxt sym ^ " -> " @@ -407,7 +407,7 @@ |> List.partition (fn sym => case Code_Symbol.Graph.get_node nodes sym of (_, Module _) => true | _ => false) - |> pairself (prioritize sym_priority) + |> apply2 (prioritize sym_priority) fun declare namify sym (nsps, nodes) = let val (base, node) = Code_Symbol.Graph.get_node nodes sym; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Tools/Code/code_preproc.ML Wed Nov 26 20:05:34 2014 +0100 @@ -267,7 +267,7 @@ in AList.make (snd o Graph.get_node eqngr) (Graph.keys eqngr) |> (map o apfst) (Code.string_of_const thy) - |> sort (string_ord o pairself fst) + |> sort (string_ord o apply2 fst) |> map (fn (s, cert) => (Pretty.block o Pretty.fbreaks) (Pretty.str s :: Code.pretty_cert thy cert)) |> Pretty.chunks end; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Tools/Code/code_target.ML Wed Nov 26 20:05:34 2014 +0100 @@ -117,11 +117,11 @@ fun cert_syms ctxt = Code_Symbol.map_attr (apfst (cert_const ctxt)) (apfst (cert_tyco ctxt)) - (apfst (cert_class ctxt)) ((apfst o pairself) (cert_class ctxt)) (apfst (cert_inst ctxt)) I; + (apfst (cert_class ctxt)) ((apfst o apply2) (cert_class ctxt)) (apfst (cert_inst ctxt)) I; fun read_syms ctxt = Code_Symbol.map_attr (apfst (read_const ctxt)) (apfst (read_tyco ctxt)) - (apfst (Proof_Context.read_class ctxt)) ((apfst o pairself) (Proof_Context.read_class ctxt)) (apfst (read_inst ctxt)) I; + (apfst (Proof_Context.read_class ctxt)) ((apfst o apply2) (Proof_Context.read_class ctxt)) (apfst (read_inst ctxt)) I; fun check_name is_module s = let diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Tools/Code/code_thingol.ML Wed Nov 26 20:05:34 2014 +0100 @@ -305,7 +305,7 @@ ((v, ty) `|=> map_terms_bottom_up f t) | map_terms_bottom_up f (ICase { term = t, typ = ty, clauses = clauses, primitive = t0 }) = f (ICase { term = map_terms_bottom_up f t, typ = ty, - clauses = (map o pairself) (map_terms_bottom_up f) clauses, + clauses = (map o apply2) (map_terms_bottom_up f) clauses, primitive = map_terms_bottom_up f t0 }); fun map_classparam_instances_as_term f = @@ -889,7 +889,7 @@ then ([], consts_of_select (Context.this_theory thy (unsuffix "._" s))) else ([Code.read_const thy str], []) | NONE => ([Code.read_const thy str], [])); - in pairself flat o split_list o map read_const_expr end; + in apply2 flat o split_list o map read_const_expr end; fun read_const_exprs_all ctxt = op @ o read_const_exprs_internal ctxt; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Tools/Spec_Check/output_style.ML --- a/src/Tools/Spec_Check/output_style.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Tools/Spec_Check/output_style.ML Wed Nov 26 20:05:34 2014 +0100 @@ -24,7 +24,7 @@ val countw = 20 val allw = namew + resultw + countw + 2 - val maybe_sort = if sort_examples then sort (int_ord o pairself size) else I + val maybe_sort = if sort_examples then sort (int_ord o apply2 size) else I fun result ({count = 0, ...}, _) _ = "dubious" | result (_ : Property.stats, badobjs) false = if null badobjs then "ok" else "FAILED" diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Tools/atomize_elim.ML --- a/src/Tools/atomize_elim.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Tools/atomize_elim.ML Wed Nov 26 20:05:34 2014 +0100 @@ -30,7 +30,7 @@ fun invert_perm pi = (pi @ subtract (op =) pi (0 upto (fold Integer.max pi 0))) |> map_index I - |> sort (int_ord o pairself snd) + |> sort (int_ord o apply2 snd) |> map fst (* rearrange_prems as a conversion *) diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Tools/cache_io.ML --- a/src/Tools/cache_io.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Tools/cache_io.ML Wed Nov 26 20:05:34 2014 +0100 @@ -98,14 +98,14 @@ else if i < p + len2 then (i+1, apsnd (cons line) xsp) else (i, xsp) val (out, err) = - pairself rev (snd (File.fold_lines load cache_path (1, ([], [])))) + apply2 rev (snd (File.fold_lines load cache_path (1, ([], [])))) in ((SOME {output = err, redirected_output = out, return_code = 0}, key), tab) end)) end fun run_and_cache (Cache {path = cache_path, table}) key make_cmd str = let val {output = err, redirected_output=out, return_code} = run make_cmd str - val (l1, l2) = pairself length (out, err) + val (l1, l2) = apply2 length (out, err) val header = key ^ " " ^ string_of_int l1 ^ " " ^ string_of_int l2 val lines = map (suffix "\n") (header :: out @ err) diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Tools/coherent.ML --- a/src/Tools/coherent.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Tools/coherent.ML Wed Nov 26 20:05:34 2014 +0100 @@ -81,7 +81,7 @@ (valid_conj ctxt facts (Pattern.match (Proof_Context.theory_of ctxt) (t, u) env) ts handle Pattern.MATCH => Seq.empty)) - (Seq.of_list (sort (int_ord o pairself snd) (Net.unify_term facts t))); + (Seq.of_list (sort (int_ord o apply2 snd) (Net.unify_term facts t))); (* Instantiate variables that only occur free in conlusion *) fun inst_extra_vars ctxt dom cs = @@ -115,7 +115,7 @@ fun string_of_facts ctxt s facts = Pretty.string_of (Pretty.big_list s - (map (Syntax.pretty_term ctxt) (map fst (sort (int_ord o pairself snd) (Net.content facts))))); + (map (Syntax.pretty_term ctxt) (map fst (sort (int_ord o apply2 snd) (Net.content facts))))); fun valid ctxt rules goal dom facts nfacts nparams = let diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Tools/induct.ML --- a/src/Tools/induct.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Tools/induct.ML Wed Nov 26 20:05:34 2014 +0100 @@ -297,7 +297,7 @@ in (context', thm') end); fun del_att which = - Thm.declaration_attribute (fn th => Data.map (which (pairself (fn rs => + Thm.declaration_attribute (fn th => Data.map (which (apply2 (fn rs => fold Item_Net.remove (filter_rules rs th) rs)))); fun add_casesT rule x = @{apply 4(1)} (apfst (Item_Net.update rule)) x; diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Tools/nbe.ML --- a/src/Tools/nbe.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Tools/nbe.ML Wed Nov 26 20:05:34 2014 +0100 @@ -64,7 +64,7 @@ val lhs_rhs = case try Logic.dest_equals eqn of SOME lhs_rhs => lhs_rhs | _ => error ("Not an equation: " ^ Syntax.string_of_term_global thy eqn); - val c_c' = case try (pairself (Axclass.unoverload_const thy o dest_Const)) lhs_rhs + val c_c' = case try (apply2 (Axclass.unoverload_const thy o dest_Const)) lhs_rhs of SOME c_c' => c_c' | _ => error ("Not an equation with two constants: " ^ Syntax.string_of_term_global thy eqn); diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Tools/subtyping.ML --- a/src/Tools/subtyping.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/Tools/subtyping.ML Wed Nov 26 20:05:34 2014 +0100 @@ -196,7 +196,7 @@ quote (Syntax.string_of_typ ctxt (Type (a, replicate (length Ts) dummyT))); fun unif (T1, T2) (env as (tye, _)) = - (case pairself (`Type_Infer.is_paramT o Type_Infer.deref tye) (T1, T2) of + (case apply2 (`Type_Infer.is_paramT o Type_Infer.deref tye) (T1, T2) of ((true, TVar (xi, S)), (_, T)) => assign xi T S env | ((_, T), (true, TVar (xi, S))) => assign xi T S env | ((_, Type (a, Ts)), (_, Type (b, Us))) => @@ -348,7 +348,7 @@ fun split_cs _ [] = ([], []) | split_cs f (c :: cs) = - (case pairself f (fst c) of + (case apply2 f (fst c) of (false, false) => apsnd (cons c) (split_cs f cs) | _ => apfst (cons c) (split_cs f cs)); @@ -392,7 +392,7 @@ val test_update = is_typeT orf is_freeT orf is_fixedvarT; val (ch, done') = done - |> map (apfst (pairself (Type_Infer.deref tye'))) + |> map (apfst (apply2 (Type_Infer.deref tye'))) |> (if not (null new) then rpair [] else split_cs test_update); val todo' = ch @ todo; in @@ -667,7 +667,8 @@ fun gen_coercion ctxt err tye TU = let - fun gen (T1, T2) = (case pairself (Type_Infer.deref tye) (T1, T2) of + fun gen (T1, T2) = + (case apply2 (Type_Infer.deref tye) (T1, T2) of (T1 as (Type (a, [])), T2 as (Type (b, []))) => if a = b then mk_identity T1 @@ -949,7 +950,7 @@ val coercions = map (fst o the o Symreltab.lookup tab) path'; val trans_co = singleton (Variable.polymorphic ctxt) (fold safe_app coercions (mk_identity dummyT)); - val (Ts, Us) = pairself (snd o Term.dest_Type) (Term.dest_funT (type_of trans_co)) + val (Ts, Us) = apply2 (snd o Term.dest_Type) (Term.dest_funT (type_of trans_co)); in (trans_co, ((Ts, Us), coercions)) end; @@ -1076,7 +1077,7 @@ val type_space = Proof_Context.type_space ctxt; val tmaps = - sort (Name_Space.extern_ord ctxt type_space o pairself #1) + sort (Name_Space.extern_ord ctxt type_space o apply2 #1) (Symtab.dest (tmaps_of ctxt)); fun show_map (c, (t, _)) = Pretty.block