renamed "pairself" to "apply2", in accordance to @{apply 2};
authorwenzelm
Wed Nov 26 20:05:34 2014 +0100 (2014-11-26)
changeset 59058a78612c67ec0
parent 59057 5b649fb2f2e1
child 59059 97b089c4aa46
renamed "pairself" to "apply2", in accordance to @{apply 2};
NEWS
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/Decision_Procs/ferrante_rackoff.ML
src/HOL/Divides.thy
src/HOL/HOLCF/Tools/Domain/domain_constructors.ML
src/HOL/HOLCF/Tools/fixrec.ML
src/HOL/Hoare/hoare_syntax.ML
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Library/Old_SMT/old_smt_normalize.ML
src/HOL/Library/Old_SMT/old_z3_model.ML
src/HOL/Library/Old_SMT/old_z3_proof_literals.ML
src/HOL/Library/Old_SMT/old_z3_proof_methods.ML
src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML
src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
src/HOL/Library/positivstellensatz.ML
src/HOL/Matrix_LP/FloatSparseMatrixBuilder.ML
src/HOL/Matrix_LP/float_arith.ML
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
src/HOL/Nitpick_Examples/Mono_Nits.thy
src/HOL/Nitpick_Examples/minipick.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_fresh_fun.ML
src/HOL/Nominal/nominal_induct.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Random.thy
src/HOL/SPARK/Tools/spark_vcs.ML
src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML
src/HOL/TPTP/atp_problem_import.ML
src/HOL/TPTP/atp_theory_export.ML
src/HOL/TPTP/mash_eval.ML
src/HOL/TPTP/mash_export.ML
src/HOL/Tools/ATP/atp_problem.ML
src/HOL/Tools/ATP/atp_problem_generate.ML
src/HOL/Tools/ATP/atp_proof.ML
src/HOL/Tools/ATP/atp_proof_reconstruct.ML
src/HOL/Tools/ATP/atp_proof_redirect.ML
src/HOL/Tools/ATP/atp_satallax.ML
src/HOL/Tools/BNF/bnf_comp.ML
src/HOL/Tools/BNF/bnf_def.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_fp_n2m.ML
src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
src/HOL/Tools/BNF/bnf_fp_util.ML
src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
src/HOL/Tools/BNF/bnf_lfp_compat.ML
src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
src/HOL/Tools/BNF/bnf_lfp_size.ML
src/HOL/Tools/BNF/bnf_tactics.ML
src/HOL/Tools/Ctr_Sugar/case_translation.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
src/HOL/Tools/Function/function_common.ML
src/HOL/Tools/Function/induction_schema.ML
src/HOL/Tools/Function/pat_completeness.ML
src/HOL/Tools/Lifting/lifting_bnf.ML
src/HOL/Tools/Lifting/lifting_def.ML
src/HOL/Tools/Lifting/lifting_info.ML
src/HOL/Tools/Meson/meson.ML
src/HOL/Tools/Meson/meson_clausify.ML
src/HOL/Tools/Metis/metis_generate.ML
src/HOL/Tools/Metis/metis_reconstruct.ML
src/HOL/Tools/Metis/metis_tactic.ML
src/HOL/Tools/Nitpick/nitpick_commands.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_kodkod.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Nitpick/nitpick_mono.ML
src/HOL/Tools/Nitpick/nitpick_nut.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
src/HOL/Tools/Nitpick/nitpick_rep.ML
src/HOL/Tools/Nitpick/nitpick_scope.ML
src/HOL/Tools/Old_Datatype/old_datatype_aux.ML
src/HOL/Tools/Old_Datatype/old_datatype_data.ML
src/HOL/Tools/Predicate_Compile/core_data.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/Quickcheck/quickcheck_common.ML
src/HOL/Tools/SMT/smt_normalize.ML
src/HOL/Tools/SMT/smtlib_interface.ML
src/HOL/Tools/SMT/z3_proof.ML
src/HOL/Tools/SMT/z3_replay_literals.ML
src/HOL/Tools/Sledgehammer/sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
src/HOL/Tools/TFL/rules.ML
src/HOL/Tools/TFL/tfl.ML
src/HOL/Tools/Transfer/transfer.ML
src/HOL/Tools/code_evaluation.ML
src/HOL/Tools/coinduction.ML
src/HOL/Tools/datatype_realizer.ML
src/HOL/Tools/functor.ML
src/HOL/Tools/hologic.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/monomorph.ML
src/HOL/Tools/record.ML
src/HOL/Tools/reification.ML
src/HOL/Tools/rewrite_hol_proof.ML
src/HOL/Tools/sat.ML
src/HOL/Tools/semiring_normalizer.ML
src/HOL/Tools/set_comprehension_pointfree.ML
src/HOL/Tools/try0.ML
src/HOL/Word/WordBitwise.thy
src/Provers/Arith/fast_lin_arith.ML
src/Provers/hypsubst.ML
src/Provers/splitter.ML
src/Pure/Concurrent/par_exn.ML
src/Pure/General/file.ML
src/Pure/General/name_space.ML
src/Pure/General/sha1_polyml.ML
src/Pure/Isar/calculation.ML
src/Pure/Isar/class.ML
src/Pure/Isar/code.ML
src/Pure/Isar/context_rules.ML
src/Pure/Isar/generic_target.ML
src/Pure/Isar/local_defs.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/rule_cases.ML
src/Pure/Isar/runtime.ML
src/Pure/ML/ml_context.ML
src/Pure/ML/ml_env.ML
src/Pure/PIDE/command.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_checker.ML
src/Pure/Proof/reconstruct.ML
src/Pure/Syntax/syntax_phases.ML
src/Pure/System/message_channel.ML
src/Pure/Thy/present.ML
src/Pure/Tools/build.ML
src/Pure/Tools/class_deps.ML
src/Pure/Tools/find_consts.ML
src/Pure/Tools/find_theorems.ML
src/Pure/Tools/plugin.ML
src/Pure/Tools/rail.ML
src/Pure/Tools/rule_insts.ML
src/Pure/Tools/thm_deps.ML
src/Pure/axclass.ML
src/Pure/context.ML
src/Pure/drule.ML
src/Pure/facts.ML
src/Pure/item_net.ML
src/Pure/library.ML
src/Pure/more_thm.ML
src/Pure/proofterm.ML
src/Pure/raw_simplifier.ML
src/Pure/search.ML
src/Pure/subgoal.ML
src/Pure/thm.ML
src/Pure/type.ML
src/Pure/type_infer_context.ML
src/Pure/variable.ML
src/Tools/Code/code_namespace.ML
src/Tools/Code/code_preproc.ML
src/Tools/Code/code_target.ML
src/Tools/Code/code_thingol.ML
src/Tools/Spec_Check/output_style.ML
src/Tools/atomize_elim.ML
src/Tools/cache_io.ML
src/Tools/coherent.ML
src/Tools/induct.ML
src/Tools/nbe.ML
src/Tools/subtyping.ML
     1.1 --- a/NEWS	Wed Nov 26 16:55:43 2014 +0100
     1.2 +++ b/NEWS	Wed Nov 26 20:05:34 2014 +0100
     1.3 @@ -224,6 +224,9 @@
     1.4  available as parameterized antiquotations, e.g. @{map 4} for lists of
     1.5  quadruples.
     1.6  
     1.7 +* Renamed "pairself" to "apply2", in accordance to @{apply 2}.
     1.8 +INCOMPATIBILITY.
     1.9 +
    1.10  
    1.11  *** System ***
    1.12  
     2.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Wed Nov 26 16:55:43 2014 +0100
     2.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Wed Nov 26 20:05:34 2014 +0100
     2.3 @@ -3502,7 +3502,7 @@
     2.4  
     2.5    fun term_of_float_float_option NONE = @{term "None :: (float \<times> float) option"}
     2.6      | term_of_float_float_option (SOME ff) = @{term "Some :: float \<times> float \<Rightarrow> _"}
     2.7 -        $ HOLogic.mk_prod (pairself term_of_float ff);
     2.8 +        $ HOLogic.mk_prod (apply2 term_of_float ff);
     2.9  
    2.10    val term_of_float_float_option_list =
    2.11      HOLogic.mk_list @{typ "(float \<times> float) option"} o map term_of_float_float_option;
    2.12 @@ -3551,7 +3551,7 @@
    2.13  
    2.14    fun float_float_option_of_term @{term "None :: (float \<times> float) option"} = NONE
    2.15      | float_float_option_of_term (@{term "Some :: float \<times> float \<Rightarrow> _"} $ ff) =
    2.16 -        SOME (pairself float_of_term (HOLogic.dest_prod ff))
    2.17 +        SOME (apply2 float_of_term (HOLogic.dest_prod ff))
    2.18      | float_float_option_of_term (@{term approx'} $ n $ a $ ffs) = @{code approx'}
    2.19          (nat_of_term n) (floatarith_of_term a) (float_float_option_list_of_term ffs)
    2.20      | float_float_option_of_term t = bad t
     3.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Nov 26 16:55:43 2014 +0100
     3.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Nov 26 20:05:34 2014 +0100
     3.3 @@ -4006,7 +4006,7 @@
     3.4  fun binopT T = T --> T --> T;
     3.5  fun relT T = T --> T --> @{typ bool};
     3.6  
     3.7 -val mk_C = @{code C} o pairself @{code int_of_integer};
     3.8 +val mk_C = @{code C} o apply2 @{code int_of_integer};
     3.9  val mk_poly_Bound = @{code poly.Bound} o @{code nat_of_integer};
    3.10  val mk_Bound = @{code Bound} o @{code nat_of_integer};
    3.11  
    3.12 @@ -4082,7 +4082,7 @@
    3.13  
    3.14  fun term_of_num T ps (@{code poly.C} (a, b)) =
    3.15        let
    3.16 -        val (c, d) = pairself (@{code integer_of_int}) (a, b)
    3.17 +        val (c, d) = apply2 (@{code integer_of_int}) (a, b)
    3.18        in
    3.19          (if d = 1 then HOLogic.mk_number T c
    3.20          else if d = 0 then Const (@{const_name Groups.zero}, T)
     4.1 --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Wed Nov 26 16:55:43 2014 +0100
     4.2 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Wed Nov 26 20:05:34 2014 +0100
     4.3 @@ -57,7 +57,7 @@
     4.4   val ((p1_v,p2_v),(mp1_v,mp2_v)) =
     4.5     funpow 2 (Thm.dest_arg o snd o Thm.dest_abs NONE)
     4.6       (funpow 4 Thm.dest_arg (cprop_of (hd minf)))
     4.7 -   |> Thm.dest_binop |> pairself Thm.dest_binop |> apfst (pairself Thm.dest_fun)
     4.8 +   |> Thm.dest_binop |> apply2 Thm.dest_binop |> apfst (apply2 Thm.dest_fun)
     4.9  
    4.10   fun myfwd (th1, th2, th3, th4, th5) p1 p2
    4.11        [(th_1,th_2,th_3,th_4,th_5), (th_1',th_2',th_3',th_4',th_5')] =
     5.1 --- a/src/HOL/Divides.thy	Wed Nov 26 16:55:43 2014 +0100
     5.2 +++ b/src/HOL/Divides.thy	Wed Nov 26 20:05:34 2014 +0100
     5.3 @@ -2104,20 +2104,23 @@
     5.4    fun binary_proc proc ctxt ct =
     5.5      (case Thm.term_of ct of
     5.6        _ $ t $ u =>
     5.7 -      (case try (pairself (`(snd o HOLogic.dest_number))) (t, u) of
     5.8 +      (case try (apply2 (`(snd o HOLogic.dest_number))) (t, u) of
     5.9          SOME args => proc ctxt args
    5.10        | NONE => NONE)
    5.11      | _ => NONE);
    5.12  in
    5.13    fun divmod_proc posrule negrule =
    5.14      binary_proc (fn ctxt => fn ((a, t), (b, u)) =>
    5.15 -      if b = 0 then NONE else let
    5.16 -        val (q, r) = pairself mk_number (Integer.div_mod a b)
    5.17 -        val goal1 = HOLogic.mk_eq (t, plus $ (times $ u $ q) $ r)
    5.18 -        val (goal2, goal3, rule) = if b > 0
    5.19 -          then (le $ zero $ r, less $ r $ u, posrule RS eq_reflection)
    5.20 -          else (le $ r $ zero, less $ u $ r, negrule RS eq_reflection)
    5.21 -      in SOME (rule OF map (prove ctxt) [goal1, goal2, goal3]) end)
    5.22 +      if b = 0 then NONE
    5.23 +      else
    5.24 +        let
    5.25 +          val (q, r) = apply2 mk_number (Integer.div_mod a b)
    5.26 +          val goal1 = HOLogic.mk_eq (t, plus $ (times $ u $ q) $ r)
    5.27 +          val (goal2, goal3, rule) =
    5.28 +            if b > 0
    5.29 +            then (le $ zero $ r, less $ r $ u, posrule RS eq_reflection)
    5.30 +            else (le $ r $ zero, less $ u $ r, negrule RS eq_reflection)
    5.31 +        in SOME (rule OF map (prove ctxt) [goal1, goal2, goal3]) end)
    5.32  end
    5.33  *}
    5.34  
     6.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Wed Nov 26 16:55:43 2014 +0100
     6.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Wed Nov 26 20:05:34 2014 +0100
     6.3 @@ -344,7 +344,7 @@
     6.4        fun dist_le (con1, args1) (con2, args2) =
     6.5          let
     6.6            val (vs1, zs1) = get_vars args1
     6.7 -          val (vs2, _) = get_vars args2 |> pairself (map prime)
     6.8 +          val (vs2, _) = get_vars args2 |> apply2 (map prime)
     6.9            val lhs = mk_below (list_ccomb (con1, vs1), list_ccomb (con2, vs2))
    6.10            val rhss = map mk_undef zs1
    6.11            val goal = mk_trp (iff_disj (lhs, rhss))
    6.12 @@ -355,7 +355,7 @@
    6.13        fun dist_eq (con1, args1) (con2, args2) =
    6.14          let
    6.15            val (vs1, zs1) = get_vars args1
    6.16 -          val (vs2, zs2) = get_vars args2 |> pairself (map prime)
    6.17 +          val (vs2, zs2) = get_vars args2 |> apply2 (map prime)
    6.18            val lhs = mk_eq (list_ccomb (con1, vs1), list_ccomb (con2, vs2))
    6.19            val rhss1 = map mk_undef zs1
    6.20            val rhss2 = map mk_undef zs2
     7.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML	Wed Nov 26 16:55:43 2014 +0100
     7.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML	Wed Nov 26 20:05:34 2014 +0100
     7.3 @@ -274,7 +274,7 @@
     7.4          | [] => fixrec_err "no defining equations for function"
     7.5          | _ => fixrec_err "all equations in block must define the same function"
     7.6      val vars =
     7.7 -        case distinct (op = o pairself length) (map fst matchers) of
     7.8 +        case distinct (op = o apply2 length) (map fst matchers) of
     7.9            [vars] => vars
    7.10          | _ => fixrec_err "all equations in block must have the same arity"
    7.11      (* rename so all matchers use same free variables *)
     8.1 --- a/src/HOL/Hoare/hoare_syntax.ML	Wed Nov 26 16:55:43 2014 +0100
     8.2 +++ b/src/HOL/Hoare/hoare_syntax.ML	Wed Nov 26 20:05:34 2014 +0100
     8.3 @@ -22,7 +22,7 @@
     8.4    | idt_name _ = NONE;
     8.5  
     8.6  fun eq_idt tu =
     8.7 -  (case pairself idt_name tu of
     8.8 +  (case apply2 idt_name tu of
     8.9      (SOME x, SOME y) => x = y
    8.10    | _ => false);
    8.11  
     9.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Nov 26 16:55:43 2014 +0100
     9.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Nov 26 20:05:34 2014 +0100
     9.3 @@ -691,7 +691,7 @@
     9.4        | imp_monad_bind (v_ty `|=> t) = v_ty `|=> imp_monad_bind t
     9.5        | imp_monad_bind (ICase { term = t, typ = ty, clauses = clauses, primitive = t0 }) =
     9.6            ICase { term = imp_monad_bind t, typ = ty,
     9.7 -            clauses = (map o pairself) imp_monad_bind clauses, primitive = imp_monad_bind t0 };
     9.8 +            clauses = (map o apply2) imp_monad_bind clauses, primitive = imp_monad_bind t0 };
     9.9  
    9.10    in (Code_Symbol.Graph.map o K o map_terms_stmt) imp_monad_bind end;
    9.11  
    10.1 --- a/src/HOL/Library/Old_SMT/old_smt_normalize.ML	Wed Nov 26 16:55:43 2014 +0100
    10.2 +++ b/src/HOL/Library/Old_SMT/old_smt_normalize.ML	Wed Nov 26 20:05:34 2014 +0100
    10.3 @@ -185,7 +185,7 @@
    10.4      if has_all_vars vs (Thm.term_of ct) then
    10.5        (case Thm.term_of ct of
    10.6          _ $ _ =>
    10.7 -          (case pairself (minimal_pats vs) (Thm.dest_comb ct) of
    10.8 +          (case apply2 (minimal_pats vs) (Thm.dest_comb ct) of
    10.9              ([], []) => [[ct]]
   10.10            | (ctss, ctss') => union (eq_set (op aconvc)) ctss ctss')
   10.11        | _ => [])
   10.12 @@ -203,7 +203,7 @@
   10.13      Old_SMT_Utils.mk_const_pat @{theory} @{const_name pat} Old_SMT_Utils.destT1
   10.14    fun mk_pat ct = Thm.apply (Old_SMT_Utils.instT' ct pat) ct
   10.15  
   10.16 -  fun mk_clist T = pairself (Thm.cterm_of @{theory})
   10.17 +  fun mk_clist T = apply2 (Thm.cterm_of @{theory})
   10.18      (HOLogic.cons_const T, HOLogic.nil_const T)
   10.19    fun mk_list (ccons, cnil) f cts = fold_rev (Thm.mk_binop ccons o f) cts cnil
   10.20    val mk_pat_list = mk_list (mk_clist @{typ pattern})
    11.1 --- a/src/HOL/Library/Old_SMT/old_z3_model.ML	Wed Nov 26 16:55:43 2014 +0100
    11.2 +++ b/src/HOL/Library/Old_SMT/old_z3_model.ML	Wed Nov 26 20:05:34 2014 +0100
    11.3 @@ -225,7 +225,7 @@
    11.4          SOME (@{const of_nat (int)}, _) => true
    11.5        | SOME (@{const nat}, _) => true
    11.6        | _ => false)
    11.7 -  in pairself (replace_vars nats) (eqs', filter_out is_coercion defs) end
    11.8 +  in apply2 (replace_vars nats) (eqs', filter_out is_coercion defs) end
    11.9  
   11.10  fun unfold_funapp (eqs, defs) =
   11.11    let
   11.12 @@ -263,13 +263,13 @@
   11.13  
   11.14      fun unfold_vars (es, ds) =
   11.15        (case first_eq rewr_var es of
   11.16 -        SOME (lr, es') => unfold_vars (pairself (replace lr) (es', ds))
   11.17 +        SOME (lr, es') => unfold_vars (apply2 (replace lr) (es', ds))
   11.18        | NONE => (es, ds))
   11.19  
   11.20      fun unfold_frees ues (es, ds) =
   11.21        (case first_eq rewr_free es of
   11.22          SOME (lr, es') =>
   11.23 -          pairself (replace lr) (es', ds)
   11.24 +          apply2 (replace lr) (es', ds)
   11.25            |> unfold_frees (HOLogic.mk_eq lr :: replace lr ues)
   11.26        | NONE => (ues @ es, ds))
   11.27  
   11.28 @@ -310,7 +310,7 @@
   11.29    | is_free_def _ = false
   11.30  
   11.31  fun defined tp =
   11.32 -  try (pairself (fst o HOLogic.dest_eq)) tp
   11.33 +  try (apply2 (fst o HOLogic.dest_eq)) tp
   11.34    |> the_default false o Option.map (op aconv)
   11.35  
   11.36  fun add_free_defs free_cs defs =
    12.1 --- a/src/HOL/Library/Old_SMT/old_z3_proof_literals.ML	Wed Nov 26 16:55:43 2014 +0100
    12.2 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_literals.ML	Wed Nov 26 20:05:34 2014 +0100
    12.3 @@ -262,7 +262,7 @@
    12.4        | NONE => 
    12.5            (case lookup_rule t of
    12.6              (rewrite, SOME lit) => (s, rewrite lit)
    12.7 -          | (_, NONE) => (s, comp (pairself join1 (dest t)))))
    12.8 +          | (_, NONE) => (s, comp (apply2 join1 (dest t)))))
    12.9  
   12.10    in snd (join1 (if is_conj then (false, t) else (true, t))) end
   12.11  
   12.12 @@ -299,7 +299,7 @@
   12.13          SOME rs => extract_lit thm rs
   12.14        | NONE =>
   12.15            the (Termtab.get_first contra_lits rules)
   12.16 -          |> pairself (extract_lit thm)
   12.17 +          |> apply2 (extract_lit thm)
   12.18            |> (fn (nlit, plit) => nlit COMP (plit COMP contra_rule)))
   12.19      end
   12.20  
    13.1 --- a/src/HOL/Library/Old_SMT/old_z3_proof_methods.ML	Wed Nov 26 16:55:43 2014 +0100
    13.2 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_methods.ML	Wed Nov 26 20:05:34 2014 +0100
    13.3 @@ -115,7 +115,7 @@
    13.4  fun prove_inj_eq ctxt ct =
    13.5    let
    13.6      val (lhs, rhs) =
    13.7 -      pairself Old_SMT_Utils.mk_cprop (Thm.dest_binop (Old_SMT_Utils.dest_cprop ct))
    13.8 +      apply2 Old_SMT_Utils.mk_cprop (Thm.dest_binop (Old_SMT_Utils.dest_cprop ct))
    13.9      val lhs_thm = Thm.implies_intr rhs (prove_lhs ctxt rhs lhs)
   13.10      val rhs_thm =
   13.11        Thm.implies_intr lhs (prove_rhs ctxt (mk_inv_def ctxt rhs) lhs rhs)
   13.12 @@ -126,7 +126,7 @@
   13.13  val swap_disj_thm = mk_meta_eq @{thm disj_commute}
   13.14  
   13.15  fun swap_conv dest eq =
   13.16 -  Old_SMT_Utils.if_true_conv ((op <) o pairself Term.size_of_term o dest)
   13.17 +  Old_SMT_Utils.if_true_conv ((op <) o apply2 Term.size_of_term o dest)
   13.18      (Conv.rewr_conv eq)
   13.19  
   13.20  val swap_eq_conv = swap_conv HOLogic.dest_eq swap_eq_thm
    14.1 --- a/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML	Wed Nov 26 16:55:43 2014 +0100
    14.2 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML	Wed Nov 26 20:05:34 2014 +0100
    14.3 @@ -287,7 +287,7 @@
    14.4      end
    14.5  
    14.6    fun dest_arg2 ct = Thm.dest_arg (Thm.dest_arg ct)
    14.7 -  fun dest ct = pairself dest_arg2 (Thm.dest_binop ct)
    14.8 +  fun dest ct = apply2 dest_arg2 (Thm.dest_binop ct)
    14.9    val contrapos =
   14.10      Old_Z3_Proof_Tools.precompose2 dest @{lemma "(~P ==> ~Q) ==> Q ==> P" by fast}
   14.11  in
   14.12 @@ -482,7 +482,7 @@
   14.13  
   14.14    fun prove_refl (ct, _) = Thm.reflexive ct
   14.15    fun prove_comb f g cp =
   14.16 -    let val ((ct1, ct2), (cu1, cu2)) = pairself Thm.dest_comb cp
   14.17 +    let val ((ct1, ct2), (cu1, cu2)) = apply2 Thm.dest_comb cp
   14.18      in Thm.combination (f (ct1, cu1)) (g (ct2, cu2)) end
   14.19    fun prove_arg f = prove_comb prove_refl f
   14.20  
   14.21 @@ -506,7 +506,7 @@
   14.22    fun prove_distinct f = prove_arg (with_length (prove_list f))
   14.23  
   14.24    fun prove_eq exn lookup cp =
   14.25 -    (case lookup (Logic.mk_equals (pairself Thm.term_of cp)) of
   14.26 +    (case lookup (Logic.mk_equals (apply2 Thm.term_of cp)) of
   14.27        SOME eq => eq
   14.28      | NONE => if exn then raise MONO else prove_refl cp)
   14.29    
    15.1 --- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Wed Nov 26 16:55:43 2014 +0100
    15.2 +++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Wed Nov 26 20:05:34 2014 +0100
    15.3 @@ -575,7 +575,7 @@
    15.4        Inttriplefunc.fold
    15.5          (fn ((b, i, j), c) => fn a => if i > j then a else ((b, i, j), c) :: a)
    15.6          m []
    15.7 -    val entss = sort (triple_int_ord o pairself fst) ents
    15.8 +    val entss = sort (triple_int_ord o apply2 fst) ents
    15.9    in
   15.10      fold_rev (fn ((b,i,j),c) => fn a =>
   15.11        pfx ^ string_of_int b ^ " " ^ string_of_int i ^ " " ^ string_of_int j ^
    16.1 --- a/src/HOL/Library/positivstellensatz.ML	Wed Nov 26 16:55:43 2014 +0100
    16.2 +++ b/src/HOL/Library/positivstellensatz.ML	Wed Nov 26 20:05:34 2014 +0100
    16.3 @@ -64,13 +64,13 @@
    16.4  structure Symfunc = FuncFun(type key = string val ord = fast_string_ord);
    16.5  structure Termfunc = FuncFun(type key = term val ord = Term_Ord.fast_term_ord);
    16.6  
    16.7 -val cterm_ord = Term_Ord.fast_term_ord o pairself term_of
    16.8 +val cterm_ord = Term_Ord.fast_term_ord o apply2 term_of
    16.9  
   16.10  structure Ctermfunc = FuncFun(type key = cterm val ord = cterm_ord);
   16.11  
   16.12  type monomial = int Ctermfunc.table;
   16.13  
   16.14 -val monomial_ord = list_ord (prod_ord cterm_ord int_ord) o pairself Ctermfunc.dest
   16.15 +val monomial_ord = list_ord (prod_ord cterm_ord int_ord) o apply2 Ctermfunc.dest
   16.16  
   16.17  structure Monomialfunc = FuncFun(type key = monomial val ord = monomial_ord)
   16.18  
   16.19 @@ -78,7 +78,7 @@
   16.20  
   16.21  (* The ordering so we can create canonical HOL polynomials.                  *)
   16.22  
   16.23 -fun dest_monomial mon = sort (cterm_ord o pairself fst) (Ctermfunc.dest mon);
   16.24 +fun dest_monomial mon = sort (cterm_ord o apply2 fst) (Ctermfunc.dest mon);
   16.25  
   16.26  fun monomial_order (m1,m2) =
   16.27    if Ctermfunc.is_empty m2 then LESS
    17.1 --- a/src/HOL/Matrix_LP/FloatSparseMatrixBuilder.ML	Wed Nov 26 16:55:43 2014 +0100
    17.2 +++ b/src/HOL/Matrix_LP/FloatSparseMatrixBuilder.ML	Wed Nov 26 20:05:34 2014 +0100
    17.3 @@ -80,7 +80,7 @@
    17.4          val eupper = HOLogic.mk_prod (index, fupper)
    17.5        in (elower :: lower, eupper :: upper) end;
    17.6    in
    17.7 -    pairself (HOLogic.mk_list spvec_elemT) (Inttab.fold app vector ([], []))
    17.8 +    apply2 (HOLogic.mk_list spvec_elemT) (Inttab.fold app vector ([], []))
    17.9    end;
   17.10  
   17.11  fun approx_matrix prec pprt vector =
   17.12 @@ -93,7 +93,7 @@
   17.13          val eupper = HOLogic.mk_prod (index, fupper)
   17.14        in (elower :: lower, eupper :: upper) end;
   17.15    in
   17.16 -    pairself (HOLogic.mk_list spmat_elemT) (Inttab.fold app vector ([], []))
   17.17 +    apply2 (HOLogic.mk_list spmat_elemT) (Inttab.fold app vector ([], []))
   17.18    end;
   17.19  
   17.20  exception Nat_expected of int;
    18.1 --- a/src/HOL/Matrix_LP/float_arith.ML	Wed Nov 26 16:55:43 2014 +0100
    18.2 +++ b/src/HOL/Matrix_LP/float_arith.ML	Wed Nov 26 20:05:34 2014 +0100
    18.3 @@ -204,10 +204,10 @@
    18.4    end
    18.5  
    18.6  fun mk_float (a, b) = @{term "float"} $
    18.7 -  HOLogic.mk_prod (pairself (HOLogic.mk_number HOLogic.intT) (a, b));
    18.8 +  HOLogic.mk_prod (apply2 (HOLogic.mk_number HOLogic.intT) (a, b));
    18.9  
   18.10  fun dest_float (Const (@{const_name float}, _) $ (Const (@{const_name Pair}, _) $ a $ b)) =
   18.11 -      pairself (snd o HOLogic.dest_number) (a, b)
   18.12 +      apply2 (snd o HOLogic.dest_number) (a, b)
   18.13    | dest_float t = ((snd o HOLogic.dest_number) t, 0);
   18.14  
   18.15  fun approx_float prec f value =
    19.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Wed Nov 26 16:55:43 2014 +0100
    19.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Wed Nov 26 20:05:34 2014 +0100
    19.3 @@ -57,7 +57,7 @@
    19.4      fun do_line line =
    19.5        (case line |> space_explode ":" of
    19.6          [line_num, offset, proof] =>
    19.7 -        SOME (pairself (the o Int.fromString) (line_num, offset),
    19.8 +        SOME (apply2 (the o Int.fromString) (line_num, offset),
    19.9                proof |> space_explode " " |> filter_out (curry (op =) ""))
   19.10         | _ => NONE)
   19.11      val proofs = File.read (Path.explode proof_file)
    20.1 --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Wed Nov 26 16:55:43 2014 +0100
    20.2 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Wed Nov 26 20:05:34 2014 +0100
    20.3 @@ -153,7 +153,7 @@
    20.4  fun theorems_of thy =
    20.5    filter (fn (name, th) =>
    20.6               not (is_forbidden_theorem name) andalso
    20.7 -             (theory_of_thm th, thy) |> pairself Context.theory_name |> op =)
    20.8 +             (theory_of_thm th, thy) |> apply2 Context.theory_name |> op =)
    20.9           (Global_Theory.all_thms_of thy true)
   20.10  
   20.11  fun check_formulas tsp =
    21.1 --- a/src/HOL/Nitpick_Examples/minipick.ML	Wed Nov 26 16:55:43 2014 +0100
    21.2 +++ b/src/HOL/Nitpick_Examples/minipick.ML	Wed Nov 26 20:05:34 2014 +0100
    21.3 @@ -123,7 +123,7 @@
    21.4          if pos andalso not (concrete T) then
    21.5            False
    21.6          else
    21.7 -          (t1, t2) |> pairself (to_R_rep Ts)
    21.8 +          (t1, t2) |> apply2 (to_R_rep Ts)
    21.9                     |> (if pos then Some o Intersect else Lone o Union)
   21.10      and to_F pos Ts t =
   21.11        (case t of
    22.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Wed Nov 26 16:55:43 2014 +0100
    22.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Nov 26 20:05:34 2014 +0100
    22.3 @@ -1664,7 +1664,7 @@
    22.4        (rec_unique_frees ~~ rec_result_Ts ~~ rec_sets);
    22.5  
    22.6      val induct_aux_rec = Drule.cterm_instantiate
    22.7 -      (map (pairself (cterm_of thy11) o apsnd (augment_sort thy11 fs_cp_sort))
    22.8 +      (map (apply2 (cterm_of thy11) o apsnd (augment_sort thy11 fs_cp_sort))
    22.9           (map (fn (aT, f) => (Logic.varify_global f, Abs ("z", HOLogic.unitT,
   22.10              Const (@{const_name Nominal.supp}, fun_tupleT --> HOLogic.mk_setT aT) $ fun_tuple)))
   22.11                fresh_fs @
    23.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Nov 26 16:55:43 2014 +0100
    23.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Nov 26 20:05:34 2014 +0100
    23.3 @@ -23,8 +23,8 @@
    23.4        (head_of (Logic.incr_indexes (Ts, j) t),
    23.5         fold_rev Term.abs ps u)) tinst;
    23.6      val th' = instf
    23.7 -      (map (pairself (ctyp_of thy)) tyinst')
    23.8 -      (map (pairself (cterm_of thy)) tinst')
    23.9 +      (map (apply2 (ctyp_of thy)) tyinst')
   23.10 +      (map (apply2 (cterm_of thy)) tinst')
   23.11        (Thm.lift_rule cgoal th)
   23.12    in
   23.13      compose_tac ctxt (elim, th', nprems_of th) i st
    24.1 --- a/src/HOL/Nominal/nominal_induct.ML	Wed Nov 26 16:55:43 2014 +0100
    24.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Wed Nov 26 20:05:34 2014 +0100
    24.3 @@ -54,7 +54,7 @@
    24.4        end;
    24.5       val substs =
    24.6         map2 subst insts concls |> flat |> distinct (op =)
    24.7 -       |> map (pairself (Thm.cterm_of (Proof_Context.theory_of ctxt)));
    24.8 +       |> map (apply2 (Thm.cterm_of (Proof_Context.theory_of ctxt)));
    24.9    in 
   24.10      (((cases, nconcls), consumes), Drule.cterm_instantiate substs joined_rule) 
   24.11    end;
    25.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Wed Nov 26 16:55:43 2014 +0100
    25.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Wed Nov 26 20:05:34 2014 +0100
    25.3 @@ -62,7 +62,7 @@
    25.4                   in (add_binders thy i u
    25.5                     (fold (fn (u, T) =>
    25.6                        if exists (fn j => j < i) (loose_bnos u) then I
    25.7 -                      else insert (op aconv o pairself fst)
    25.8 +                      else insert (op aconv o apply2 fst)
    25.9                          (incr_boundvars (~i) u, T)) cargs1 bs'), cargs2)
   25.10                   end) cargs (bs, ts ~~ Ts))))
   25.11        | _ => fold (add_binders thy i) ts bs)
   25.12 @@ -164,7 +164,7 @@
   25.13        HOLogic.dest_conj |> map (HOLogic.dest_imp ##> strip_comb);
   25.14      val ps = map (fst o snd) concls;
   25.15  
   25.16 -    val _ = (case duplicates (op = o pairself fst) avoids of
   25.17 +    val _ = (case duplicates (op = o apply2 fst) avoids of
   25.18          [] => ()
   25.19        | xs => error ("Duplicate case names: " ^ commas_quote (map fst xs)));
   25.20      val _ = avoids |> forall (fn (a, xs) => null (duplicates (op =) xs) orelse
   25.21 @@ -338,7 +338,7 @@
   25.22                   val pis'' = fold (concat_perm #> map) pis' pis;
   25.23                   val env = Pattern.first_order_match thy (ihypt, prop_of ihyp)
   25.24                     (Vartab.empty, Vartab.empty);
   25.25 -                 val ihyp' = Thm.instantiate ([], map (pairself (cterm_of thy))
   25.26 +                 val ihyp' = Thm.instantiate ([], map (apply2 (cterm_of thy))
   25.27                     (map (Envir.subst_term env) vs ~~
   25.28                      map (fold_rev (NominalDatatype.mk_perm [])
   25.29                        (rev pis' @ pis)) params' @ [z])) ihyp;
    26.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Wed Nov 26 16:55:43 2014 +0100
    26.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Wed Nov 26 20:05:34 2014 +0100
    26.3 @@ -173,7 +173,7 @@
    26.4        HOLogic.dest_conj |> map (HOLogic.dest_imp ##> strip_comb);
    26.5      val ps = map (fst o snd) concls;
    26.6  
    26.7 -    val _ = (case duplicates (op = o pairself fst) avoids of
    26.8 +    val _ = (case duplicates (op = o apply2 fst) avoids of
    26.9          [] => ()
   26.10        | xs => error ("Duplicate case names: " ^ commas_quote (map fst xs)));
   26.11      val _ = (case subtract (op =) induct_cases (map fst avoids) of
    27.1 --- a/src/HOL/Random.thy	Wed Nov 26 16:55:43 2014 +0100
    27.2 +++ b/src/HOL/Random.thy	Wed Nov 26 20:05:34 2014 +0100
    27.3 @@ -156,7 +156,7 @@
    27.4      val now = Time.toMilliseconds (Time.now ());
    27.5      val (q, s1) = IntInf.divMod (now, 2147483562);
    27.6      val s2 = q mod 2147483398;
    27.7 -  in pairself Code_Numeral.natural_of_integer (s1 + 1, s2 + 1) end);
    27.8 +  in apply2 Code_Numeral.natural_of_integer (s1 + 1, s2 + 1) end);
    27.9  
   27.10  in
   27.11  
    28.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Wed Nov 26 16:55:43 2014 +0100
    28.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Wed Nov 26 20:05:34 2014 +0100
    28.3 @@ -33,10 +33,10 @@
    28.4  
    28.5  fun err_unfinished () = error "An unfinished SPARK environment is still open."
    28.6  
    28.7 -val strip_number = pairself implode o take_suffix Fdl_Lexer.is_digit o raw_explode;
    28.8 +val strip_number = apply2 implode o take_suffix Fdl_Lexer.is_digit o raw_explode;
    28.9  
   28.10  val name_ord = prod_ord string_ord (option_ord int_ord) o
   28.11 -  pairself (strip_number ##> Int.fromString);
   28.12 +  apply2 (strip_number ##> Int.fromString);
   28.13  
   28.14  structure VCtab = Table(type key = string val ord = name_ord);
   28.15  
   28.16 @@ -72,7 +72,7 @@
   28.17  
   28.18  val to_lower = raw_explode #> map Symbol.to_ascii_lower #> implode;
   28.19  
   28.20 -val lcase_eq = (op =) o pairself (to_lower o Long_Name.base_name);
   28.21 +val lcase_eq = (op =) o apply2 (to_lower o Long_Name.base_name);
   28.22  
   28.23  fun lookup_prfx "" tab s = Symtab.lookup tab s
   28.24    | lookup_prfx prfx tab s = (case Symtab.lookup tab s of
   28.25 @@ -366,7 +366,7 @@
   28.26                | SOME {fields, ...} =>
   28.27                    let val fields' = invert_map cmap fields
   28.28                    in
   28.29 -                    (case subtract (lcase_eq o pairself fst) fldTs fields' of
   28.30 +                    (case subtract (lcase_eq o apply2 fst) fldTs fields' of
   28.31                         [] => ()
   28.32                       | flds => assoc_ty_err thy rT s ("has extra field(s) " ^
   28.33                           commas (map (Long_Name.base_name o fst) flds));
   28.34 @@ -862,8 +862,8 @@
   28.35  
   28.36  fun check_mapping _ _ [] _ = ()
   28.37    | check_mapping err s cmap cs =
   28.38 -      (case duplicates (op = o pairself fst) cmap of
   28.39 -         [] => (case duplicates (op = o pairself snd) cmap of
   28.40 +      (case duplicates (op = o apply2 fst) cmap of
   28.41 +         [] => (case duplicates (op = o apply2 snd) cmap of
   28.42               [] => (case subtract (op = o apsnd snd) cs cmap of
   28.43                   [] => (case subtract (op = o apfst snd) cmap cs of
   28.44                       [] => ()
    29.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML	Wed Nov 26 16:55:43 2014 +0100
    29.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML	Wed Nov 26 20:05:34 2014 +0100
    29.3 @@ -574,14 +574,14 @@
    29.4        diff thy (scheme_t, instance_t)
    29.5  
    29.6      (*valuation of type variables*)
    29.7 -    val typeval = map (pairself (ctyp_of thy)) type_pairing
    29.8 +    val typeval = map (apply2 (ctyp_of thy)) type_pairing
    29.9  
   29.10      val typeval_env =
   29.11        map (apfst dest_TVar) type_pairing
   29.12      (*valuation of term variables*)
   29.13      val termval =
   29.14        map (apfst (type_devar typeval_env)) term_pairing
   29.15 -      |> map (pairself (cterm_of thy))
   29.16 +      |> map (apply2 (cterm_of thy))
   29.17    in
   29.18      Thm.instantiate (typeval, termval) scheme_thm
   29.19    end
    30.1 --- a/src/HOL/TPTP/atp_problem_import.ML	Wed Nov 26 16:55:43 2014 +0100
    30.2 +++ b/src/HOL/TPTP/atp_problem_import.ML	Wed Nov 26 20:05:34 2014 +0100
    30.3 @@ -56,7 +56,7 @@
    30.4        ||> List.partition (has_role TPTP_Syntax.Role_Definition)
    30.5    in
    30.6      (map (get_prop I) conjs,
    30.7 -     pairself (map (get_prop Logic.varify_global)) defs_and_nondefs,
    30.8 +     apply2 (map (get_prop Logic.varify_global)) defs_and_nondefs,
    30.9       Named_Target.theory_init thy)
   30.10    end
   30.11  
    31.1 --- a/src/HOL/TPTP/atp_theory_export.ML	Wed Nov 26 16:55:43 2014 +0100
    31.2 +++ b/src/HOL/TPTP/atp_theory_export.ML	Wed Nov 26 20:05:34 2014 +0100
    31.3 @@ -127,7 +127,7 @@
    31.4    | ident_of_problem_line (Class_Memb (ident, _, _, _)) = ident
    31.5    | ident_of_problem_line (Formula ((ident, _), _, _, _, _)) = ident
    31.6  
    31.7 -fun order_facts ord = sort (ord o pairself ident_of_problem_line)
    31.8 +fun order_facts ord = sort (ord o apply2 ident_of_problem_line)
    31.9  
   31.10  fun order_problem_facts _ [] = []
   31.11    | order_problem_facts ord ((heading, lines) :: problem) =
   31.12 @@ -166,7 +166,7 @@
   31.13      val facts =
   31.14        Sledgehammer_Fact.all_facts (Proof_Context.init_global thy) true false
   31.15                                    Keyword.empty_keywords [] [] css_table
   31.16 -      |> sort (Sledgehammer_MaSh.crude_thm_ord o pairself snd)
   31.17 +      |> sort (Sledgehammer_MaSh.crude_thm_ord o apply2 snd)
   31.18      val problem =
   31.19        facts
   31.20        |> map (fn ((_, loc), th) =>
   31.21 @@ -202,7 +202,7 @@
   31.22      val order_tab =
   31.23        Symtab.empty
   31.24        |> fold (Symtab.insert (op =)) (ordered_names ~~ (1 upto length ordered_names))
   31.25 -    val name_ord = int_ord o pairself (the o Symtab.lookup order_tab)
   31.26 +    val name_ord = int_ord o apply2 (the o Symtab.lookup order_tab)
   31.27    in
   31.28      problem
   31.29      |> (case format of
   31.30 @@ -297,7 +297,7 @@
   31.31        problem_of_theory ctxt thy format infer_policy type_enc
   31.32        |> split_last
   31.33        ||> (snd
   31.34 -           #> chop_maximal_groups (op = o pairself theory_name_of_fact)
   31.35 +           #> chop_maximal_groups (op = o apply2 theory_name_of_fact)
   31.36             #> map (`(include_base_name_of_fact o hd)))
   31.37      fun write_prelude () =
   31.38        let val ss = lines_of_problem ctxt format prelude in
    32.1 --- a/src/HOL/TPTP/mash_eval.ML	Wed Nov 26 16:55:43 2014 +0100
    32.2 +++ b/src/HOL/TPTP/mash_eval.ML	Wed Nov 26 20:05:34 2014 +0100
    32.3 @@ -66,7 +66,7 @@
    32.4          (if is_none outcome then
    32.5             "Success (" ^ ATP_Util.string_of_time run_time ^ "): " ^
    32.6             (used_facts |> map (with_index facts o fst)
    32.7 -                       |> sort (int_ord o pairself fst)
    32.8 +                       |> sort (int_ord o apply2 fst)
    32.9                         |> map index_str
   32.10                         |> space_implode " ") ^
   32.11             (if length facts < the max_facts then
    33.1 --- a/src/HOL/TPTP/mash_export.ML	Wed Nov 26 16:55:43 2014 +0100
    33.2 +++ b/src/HOL/TPTP/mash_export.ML	Wed Nov 26 20:05:34 2014 +0100
    33.3 @@ -65,7 +65,7 @@
    33.4  fun all_facts ctxt =
    33.5    let val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt in
    33.6      Sledgehammer_Fact.all_facts ctxt true false Keyword.empty_keywords [] [] css
    33.7 -    |> sort (crude_thm_ord o pairself snd)
    33.8 +    |> sort (crude_thm_ord o apply2 snd)
    33.9    end
   33.10  
   33.11  fun filter_accessible_from th = filter (fn (_, th') => thm_less (th', th))
    34.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Wed Nov 26 16:55:43 2014 +0100
    34.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Wed Nov 26 20:05:34 2014 +0100
    34.3 @@ -304,7 +304,7 @@
    34.4    | raw_polarities_of_conn AIff = (NONE, NONE)
    34.5  fun polarities_of_conn NONE = K (NONE, NONE)
    34.6    | polarities_of_conn (SOME pos) =
    34.7 -    raw_polarities_of_conn #> not pos ? pairself (Option.map not)
    34.8 +    raw_polarities_of_conn #> not pos ? apply2 (Option.map not)
    34.9  
   34.10  fun mk_anot (AConn (ANot, [phi])) = phi
   34.11    | mk_anot phi = AConn (ANot, [phi])
   34.12 @@ -776,10 +776,10 @@
   34.13  fun clausify_formula pos (phi as AAtom _) = [phi |> not pos ? mk_anot]
   34.14    | clausify_formula pos (AConn (ANot, [phi])) = clausify_formula (not pos) phi
   34.15    | clausify_formula true (AConn (AOr, [phi1, phi2])) =
   34.16 -    (phi1, phi2) |> pairself (clausify_formula true)
   34.17 +    (phi1, phi2) |> apply2 (clausify_formula true)
   34.18                   |> uncurry (map_product (mk_aconn AOr))
   34.19    | clausify_formula false (AConn (AAnd, [phi1, phi2])) =
   34.20 -    (phi1, phi2) |> pairself (clausify_formula false)
   34.21 +    (phi1, phi2) |> apply2 (clausify_formula false)
   34.22                   |> uncurry (map_product (mk_aconn AOr))
   34.23    | clausify_formula true (AConn (AImplies, [phi1, phi2])) =
   34.24      clausify_formula true (AConn (AOr, [mk_anot phi1, phi2]))
    35.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Nov 26 16:55:43 2014 +0100
    35.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Nov 26 20:05:34 2014 +0100
    35.3 @@ -789,8 +789,8 @@
    35.4    (facts, lifted)
    35.5    (* Lambda-lifting sometimes leaves some lambdas around; we need some way to
    35.6       get rid of them *)
    35.7 -  |> pairself (map (introduce_combinators ctxt))
    35.8 -  |> pairself (map constify_lifted)
    35.9 +  |> apply2 (map (introduce_combinators ctxt))
   35.10 +  |> apply2 (map constify_lifted)
   35.11    (* Requires bound variables not to clash with any schematic variables (as
   35.12       should be the case right after lambda-lifting). *)
   35.13    |>> map (hol_open_form (unprefix hol_close_form_prefix))
   35.14 @@ -1317,7 +1317,7 @@
   35.15          []
   35.16        else
   35.17          0 upto length footprint - 1 ~~ footprint
   35.18 -        |> sort (rev_order o list_ord Term_Ord.indexname_ord o pairself snd)
   35.19 +        |> sort (rev_order o list_ord Term_Ord.indexname_ord o apply2 snd)
   35.20          |> cover []
   35.21      end
   35.22  
   35.23 @@ -1752,7 +1752,7 @@
   35.24                   ths ~~ (1 upto length ths)
   35.25                   |> maps (dub_and_inst needs_sound o apfst (apsnd prop_of))
   35.26                   |> make_facts
   35.27 -                 |> union (op = o pairself #iformula))
   35.28 +                 |> union (op = o apply2 #iformula))
   35.29             (if completish then completish_helper_table else helper_table)
   35.30      end
   35.31    | NONE => I)
   35.32 @@ -1860,7 +1860,7 @@
   35.33        |> map2 (pair o rpair (Local, General) o string_of_int) (0 upto length hyp_ts)
   35.34      val ((conjs, facts), lam_facts) =
   35.35        (conjs, facts)
   35.36 -      |> presimp ? pairself (map (apsnd (apsnd (presimp_prop ctxt type_enc))))
   35.37 +      |> presimp ? apply2 (map (apsnd (apsnd (presimp_prop ctxt type_enc))))
   35.38        |> (if lam_trans = no_lamsN then
   35.39              rpair []
   35.40            else
   35.41 @@ -2604,7 +2604,7 @@
   35.42      fun firstorderize in_helper =
   35.43        firstorderize_fact thy ctrss type_enc (uncurried_aliases andalso not in_helper) completish
   35.44          sym_tab0
   35.45 -    val (conjs, facts) = (conjs, facts) |> pairself (map (firstorderize false))
   35.46 +    val (conjs, facts) = (conjs, facts) |> apply2 (map (firstorderize false))
   35.47      val (ho_stuff, sym_tab) =
   35.48        sym_table_of_facts ctxt type_enc Min_App_Op conjs facts
   35.49      val (uncurried_alias_eq_tms, uncurried_alias_eq_lines) =
   35.50 @@ -2705,7 +2705,7 @@
   35.51      |> fold (fold (add_line_weights type_info_default_weight) o get)
   35.52              [explicit_declsN, subclassesN, tconsN]
   35.53      |> Symtab.dest
   35.54 -    |> sort (prod_ord Real.compare string_ord o pairself swap)
   35.55 +    |> sort (prod_ord Real.compare string_ord o apply2 swap)
   35.56    end
   35.57  
   35.58  (* Ugly hack: may make innocent victims (collateral damage) *)
   35.59 @@ -2733,8 +2733,7 @@
   35.60  
   35.61  fun strip_iff_etc (ATyQuant (_, _, phi)) = strip_iff_etc phi
   35.62    | strip_iff_etc (AQuant (_, _, phi)) = strip_iff_etc phi
   35.63 -  | strip_iff_etc (AConn (AIff, [phi1, phi2])) =
   35.64 -    pairself strip_up_to_predicator (phi1, phi2)
   35.65 +  | strip_iff_etc (AConn (AIff, [phi1, phi2])) = apply2 strip_up_to_predicator (phi1, phi2)
   35.66    | strip_iff_etc _ = ([], [])
   35.67  
   35.68  val max_term_order_weight = 2147483647
   35.69 @@ -2800,7 +2799,7 @@
   35.70    in
   35.71      (* Sorting is not just for aesthetics: It specifies the precedence order for
   35.72         the term ordering (KBO or LPO), from smaller to larger values. *)
   35.73 -    [] |> add_weights 1 (Graph.minimals graph) |> sort (int_ord o pairself snd)
   35.74 +    [] |> add_weights 1 (Graph.minimals graph) |> sort (int_ord o apply2 snd)
   35.75    end
   35.76  
   35.77  end;
    36.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Nov 26 16:55:43 2014 +0100
    36.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Nov 26 20:05:34 2014 +0100
    36.3 @@ -243,7 +243,7 @@
    36.4  
    36.5  (* Splits by the first possible of a list of delimiters. *)
    36.6  fun extract_tstplike_proof delims output =
    36.7 -  (case pairself (find_first (fn s => String.isSubstring s output)) (ListPair.unzip delims) of
    36.8 +  (case apply2 (find_first (fn s => String.isSubstring s output)) (ListPair.unzip delims) of
    36.9      (SOME begin_delim, SOME end_delim) => extract_delimited (begin_delim, end_delim) output
   36.10    | _ => "")
   36.11  
   36.12 @@ -269,9 +269,9 @@
   36.13  val vampire_fact_prefix = "f"
   36.14  
   36.15  fun vampire_step_name_ord p =
   36.16 -  let val q = pairself fst p in
   36.17 +  let val q = apply2 fst p in
   36.18      (* The "unprefix" part is to cope with Vampire's output. *)
   36.19 -    (case pairself (Int.fromString o perhaps (try (unprefix vampire_fact_prefix))) q of
   36.20 +    (case apply2 (Int.fromString o perhaps (try (unprefix vampire_fact_prefix))) q of
   36.21        (SOME i, SOME j) => int_ord (i, j)
   36.22      | _ => raise Fail "not Vampire")
   36.23    end
   36.24 @@ -286,8 +286,8 @@
   36.25     with "$" and possibly with "!" in them (for "z3_tptp"). *)
   36.26  val scan_general_id =
   36.27    $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode
   36.28 -  || (Scan.repeat ($$ "$") -- Scan.many1 Symbol.is_letdig >> (op ^ o pairself implode))
   36.29 -    -- Scan.optional (Scan.repeat ($$ "!") -- Scan.many1 Symbol.is_letdig >> (op ^ o pairself implode)) ""
   36.30 +  || (Scan.repeat ($$ "$") -- Scan.many1 Symbol.is_letdig >> (op ^ o apply2 implode))
   36.31 +    -- Scan.optional (Scan.repeat ($$ "!") -- Scan.many1 Symbol.is_letdig >> (op ^ o apply2 implode)) ""
   36.32      >> op ^
   36.33  
   36.34  val skip_term =
   36.35 @@ -429,7 +429,7 @@
   36.36                else K NONE)
   36.37            end
   36.38        | do_term_pair (ATerm ((s1, _), args1)) (ATerm ((s2, _), args2)) (SOME subst) =
   36.39 -        (case pairself is_tptp_variable (s1, s2) of
   36.40 +        (case apply2 is_tptp_variable (s1, s2) of
   36.41            (true, true) =>
   36.42            (case AList.lookup (op =) subst s1 of
   36.43              SOME s2' => if s2' = s2 then SOME subst else NONE
    37.1 --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed Nov 26 16:55:43 2014 +0100
    37.2 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed Nov 26 20:05:34 2014 +0100
    37.3 @@ -674,7 +674,7 @@
    37.4              val (haves, have_nots) =
    37.5                HOLogic.disjuncts t
    37.6                |> List.partition (exists_subterm (curry (op =) (Var v)))
    37.7 -              |> pairself (fn lits => fold (curry s_disj) lits @{term False})
    37.8 +              |> apply2 (fn lits => fold (curry s_disj) lits @{term False})
    37.9            in
   37.10              s_disj (HOLogic.all_const T
   37.11                  $ Abs (s, T, unskolem (safe_abstract_over (Var v, kill_skolem_arg haves))),
    38.1 --- a/src/HOL/Tools/ATP/atp_proof_redirect.ML	Wed Nov 26 16:55:43 2014 +0100
    38.2 +++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML	Wed Nov 26 20:05:34 2014 +0100
    38.3 @@ -68,7 +68,7 @@
    38.4  
    38.5  val atom_eq = is_equal o Atom.ord
    38.6  val clause_ord = dict_ord Atom.ord
    38.7 -fun direct_sequent_ord seqp = prod_ord clause_ord clause_ord (pairself snd seqp)
    38.8 +fun direct_sequent_ord seqp = prod_ord clause_ord clause_ord (apply2 snd seqp)
    38.9  fun direct_sequent_eq seqp = is_equal (direct_sequent_ord seqp)
   38.10  
   38.11  fun make_refute_graph bot infers =
    39.1 --- a/src/HOL/Tools/ATP/atp_satallax.ML	Wed Nov 26 16:55:43 2014 +0100
    39.2 +++ b/src/HOL/Tools/ATP/atp_satallax.ML	Wed Nov 26 20:05:34 2014 +0100
    39.3 @@ -426,7 +426,7 @@
    39.4      | NONE =>
    39.5        tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
    39.6        |> parse_proof local_prover problem
    39.7 -      |> local_prover = vampireN ? perhaps (try (sort (vampire_step_name_ord o pairself #1)))
    39.8 +      |> local_prover = vampireN ? perhaps (try (sort (vampire_step_name_ord o apply2 #1)))
    39.9        |> local_prover = zipperpositionN ? rev)
   39.10  
   39.11  end;
    40.1 --- a/src/HOL/Tools/BNF/bnf_comp.ML	Wed Nov 26 16:55:43 2014 +0100
    40.2 +++ b/src/HOL/Tools/BNF/bnf_comp.ML	Wed Nov 26 20:05:34 2014 +0100
    40.3 @@ -655,7 +655,7 @@
    40.4    end;
    40.5  
    40.6  fun default_comp_sort Ass =
    40.7 -  Library.sort (Term_Ord.typ_ord o pairself TFree) (fold (fold (insert (op =))) Ass []);
    40.8 +  Library.sort (Term_Ord.typ_ord o apply2 TFree) (fold (fold (insert (op =))) Ass []);
    40.9  
   40.10  fun raw_compose_bnf const_policy qualify flatten_tyargs outer inners oDs Dss tfreess accum =
   40.11    let
   40.12 @@ -914,7 +914,7 @@
   40.13              val lives = lives_of_bnf bnf;
   40.14              val tvars' = Term.add_tvarsT T' [];
   40.15              val Ds_As =
   40.16 -              pairself (map (Term.typ_subst_TVars (map fst tvars' ~~ map TFree tfrees)))
   40.17 +              apply2 (map (Term.typ_subst_TVars (map fst tvars' ~~ map TFree tfrees)))
   40.18                  (deads, lives);
   40.19            in ((bnf, Ds_As), accum) end
   40.20          else
    41.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Wed Nov 26 16:55:43 2014 +0100
    41.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Wed Nov 26 20:05:34 2014 +0100
    41.3 @@ -782,7 +782,7 @@
    41.4        end;
    41.5  
    41.6      fun maybe_restore lthy_old lthy =
    41.7 -      lthy |> not (Theory.eq_thy (pairself Proof_Context.theory_of (lthy_old, lthy)))
    41.8 +      lthy |> not (Theory.eq_thy (apply2 Proof_Context.theory_of (lthy_old, lthy)))
    41.9          ? Local_Theory.restore;
   41.10  
   41.11      val map_bind_def =
    42.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Nov 26 16:55:43 2014 +0100
    42.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Nov 26 20:05:34 2014 +0100
    42.3 @@ -2167,7 +2167,7 @@
    42.4              val sel_bTs =
    42.5                flat sel_bindingss ~~ flat sel_Tss
    42.6                |> filter_out (Binding.is_empty o fst)
    42.7 -              |> distinct (Binding.eq_name o pairself fst);
    42.8 +              |> distinct (Binding.eq_name o apply2 fst);
    42.9              val sel_default_lthy = fake_local_theory_for_sel_defaults sel_bTs lthy;
   42.10  
   42.11              val sel_default_eqs = map (prepare_term sel_default_lthy) raw_sel_default_eqs;
    43.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Nov 26 16:55:43 2014 +0100
    43.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Nov 26 20:05:34 2014 +0100
    43.3 @@ -74,7 +74,7 @@
    43.4      val nesting_bnfss =
    43.5        map (fn sugar => #fp_nesting_bnfs sugar @ #live_nesting_bnfs sugar) fp_sugars;
    43.6      val fp_or_nesting_bnfss = fp_bnfs :: nesting_bnfss;
    43.7 -    val fp_or_nesting_bnfs = distinct (op = o pairself T_of_bnf) (flat fp_or_nesting_bnfss);
    43.8 +    val fp_or_nesting_bnfs = distinct (op = o apply2 T_of_bnf) (flat fp_or_nesting_bnfss);
    43.9  
   43.10      val fp_absTs = map #absT fp_absT_infos;
   43.11      val fp_repTs = map #repT fp_absT_infos;
   43.12 @@ -139,7 +139,7 @@
   43.13      val rels =
   43.14        let
   43.15          fun find_rel T As Bs = fp_or_nesting_bnfss
   43.16 -          |> map (filter_out (curry (op = o pairself name_of_bnf) BNF_Comp.DEADID_bnf))
   43.17 +          |> map (filter_out (curry (op = o apply2 name_of_bnf) BNF_Comp.DEADID_bnf))
   43.18            |> get_first (find_first (fn bnf => Type.could_unify (T_of_bnf bnf, T)))
   43.19            |> Option.map (fn bnf =>
   43.20              let val live = live_of_bnf bnf;
   43.21 @@ -191,7 +191,7 @@
   43.22            case_fp fp (snd o Term.dest_comb) (snd o Term.dest_comb o fst o Term.dest_comb);
   43.23          val raw_phis = map (extract o HOLogic.dest_Trueprop o Thm.concl_of) rel_xtor_co_inducts;
   43.24          val thetas = AList.group (op =)
   43.25 -          (mutual_cliques ~~ map (pairself (certify lthy)) (raw_phis ~~ pre_phis));
   43.26 +          (mutual_cliques ~~ map (apply2 (certify lthy)) (raw_phis ~~ pre_phis));
   43.27        in
   43.28          map2 (Drule.cterm_instantiate o the o AList.lookup (op =) thetas)
   43.29          mutual_cliques rel_xtor_co_inducts
   43.30 @@ -286,7 +286,7 @@
   43.31  
   43.32          val fold_pre_deads_only_Ts =
   43.33            map (typ_subst_nonatomic_sorted (map (rpair dummyT)
   43.34 -            (As @ sort (int_ord o pairself Term.size_of_typ) fpTs))) fold_preTs';
   43.35 +            (As @ sort (int_ord o apply2 Term.size_of_typ) fpTs))) fold_preTs';
   43.36  
   43.37          val (mutual_clique, TUs) =
   43.38            map_split dest_co_algT (binder_fun_types (foldT_of_recT (fastype_of approx_rec)))
   43.39 @@ -439,7 +439,7 @@
   43.40            @{thms fst_convol map_prod_o_convol convol_o fst_comp_map_prod}
   43.41            @{thms case_sum_o_inj(1) case_sum_o_map_sum o_case_sum map_sum_o_inj(1)};
   43.42  
   43.43 -        val eq_thm_prop_untyped = Term.aconv_untyped o pairself Thm.full_prop_of;
   43.44 +        val eq_thm_prop_untyped = Term.aconv_untyped o apply2 Thm.full_prop_of;
   43.45  
   43.46          val map_thms = no_refl (maps (fn bnf =>
   43.47             let val map_comp0 = map_comp0_of_bnf bnf RS sym
    44.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Wed Nov 26 16:55:43 2014 +0100
    44.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Wed Nov 26 20:05:34 2014 +0100
    44.3 @@ -390,7 +390,7 @@
    44.4          (if Ts1 = Ts2 andalso length Ts1 = 1 then "itself" else qsotys Ts2));
    44.5  
    44.6      val sorted_actual_Ts =
    44.7 -      sort (prod_ord int_ord Term_Ord.typ_ord o pairself (`Term.size_of_typ)) actual_Ts;
    44.8 +      sort (prod_ord int_ord Term_Ord.typ_ord o apply2 (`Term.size_of_typ)) actual_Ts;
    44.9  
   44.10      fun the_ctrs_of (Type (s, Ts)) = map (mk_ctr Ts) (#ctrs (the (ctr_sugar_of lthy s)));
   44.11  
    45.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Wed Nov 26 16:55:43 2014 +0100
    45.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Wed Nov 26 20:05:34 2014 +0100
    45.3 @@ -578,7 +578,7 @@
    45.4      val n = Thm.nprems_of coind;
    45.5      val m = Thm.nprems_of (hd rel_monos) - n;
    45.6      fun mk_inst phi = (phi, mk_union (phi, HOLogic.eq_const (fst (dest_pred2T (fastype_of phi)))))
    45.7 -      |> pairself (certify ctxt);
    45.8 +      |> apply2 (certify ctxt);
    45.9      val insts = Term.add_vars (Thm.prop_of coind) [] |> rev |> take n |> map (mk_inst o Var);
   45.10      fun mk_unfold rel_eq rel_mono =
   45.11        let
    46.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Wed Nov 26 16:55:43 2014 +0100
    46.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Wed Nov 26 20:05:34 2014 +0100
    46.3 @@ -128,7 +128,7 @@
    46.4  fun unexpected_corec_call ctxt t =
    46.5    error ("Unexpected corecursive call: " ^ quote (Syntax.string_of_term ctxt t));
    46.6  
    46.7 -fun sort_list_duplicates xs = map snd (sort (int_ord o pairself fst) xs);
    46.8 +fun sort_list_duplicates xs = map snd (sort (int_ord o apply2 fst) xs);
    46.9  
   46.10  val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default @{const True};
   46.11  val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default @{const False};
   46.12 @@ -415,7 +415,7 @@
   46.13      val coinduct_attrs_pair =
   46.14        (case gfp_sugar_thms of SOME ((_, attrs_pair), _, _, _, _) => attrs_pair | NONE => ([], []));
   46.15  
   46.16 -    val perm_fp_sugars = sort (int_ord o pairself #fp_res_index) fp_sugars;
   46.17 +    val perm_fp_sugars = sort (int_ord o apply2 #fp_res_index) fp_sugars;
   46.18  
   46.19      val indices = map #fp_res_index fp_sugars;
   46.20      val perm_indices = map #fp_res_index perm_fp_sugars;
   46.21 @@ -998,7 +998,7 @@
   46.22  
   46.23      val callssss =
   46.24        map_filter (try (fn Sel x => x)) eqns_data
   46.25 -      |> partition_eq (op = o pairself #fun_name)
   46.26 +      |> partition_eq (op = o apply2 #fun_name)
   46.27        |> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names
   46.28        |> map (flat o snd)
   46.29        |> map2 (fold o find_corec_calls lthy has_call) basic_ctr_specss
   46.30 @@ -1012,21 +1012,24 @@
   46.31      val ctr_specss = map #ctr_specs corec_specs;
   46.32  
   46.33      val disc_eqnss' = map_filter (try (fn Disc x => x)) eqns_data
   46.34 -      |> partition_eq (op = o pairself #fun_name)
   46.35 +      |> partition_eq (op = o apply2 #fun_name)
   46.36        |> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names
   46.37 -      |> map (sort (op < o pairself #ctr_no |> make_ord) o flat o snd);
   46.38 +      |> map (sort (op < o apply2 #ctr_no |> make_ord) o flat o snd);
   46.39  
   46.40      val _ = disc_eqnss' |> map (fn x =>
   46.41 -      let val d = duplicates (op = o pairself #ctr_no) x in null d orelse
   46.42 -        (if forall (is_some o #ctr_rhs_opt) x then
   46.43 -          primcorec_error_eqns "multiple equations for constructor(s)"
   46.44 -            (maps (fn t => filter (curry (op =) (#ctr_no t) o #ctr_no) x) d
   46.45 -              |> map (the o #ctr_rhs_opt)) else
   46.46 -          primcorec_error_eqns "excess discriminator formula in definition"
   46.47 -            (maps (fn t => filter (curry (op =) (#ctr_no t) o #ctr_no) x) d |> map #user_eqn)) end);
   46.48 +      let val d = duplicates (op = o apply2 #ctr_no) x in
   46.49 +        null d orelse
   46.50 +         (if forall (is_some o #ctr_rhs_opt) x then
   46.51 +            primcorec_error_eqns "multiple equations for constructor(s)"
   46.52 +              (maps (fn t => filter (curry (op =) (#ctr_no t) o #ctr_no) x) d
   46.53 +                |> map (the o #ctr_rhs_opt))
   46.54 +          else
   46.55 +            primcorec_error_eqns "excess discriminator formula in definition"
   46.56 +              (maps (fn t => filter (curry (op =) (#ctr_no t) o #ctr_no) x) d |> map #user_eqn))
   46.57 +      end);
   46.58  
   46.59      val sel_eqnss = map_filter (try (fn Sel x => x)) eqns_data
   46.60 -      |> partition_eq (op = o pairself #fun_name)
   46.61 +      |> partition_eq (op = o apply2 #fun_name)
   46.62        |> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names
   46.63        |> map (flat o snd);
   46.64  
   46.65 @@ -1316,7 +1319,7 @@
   46.66                    let
   46.67                      val ms = map (Logic.count_prems o prop_of) ctr_thms;
   46.68                      val (raw_goal, goal) = (raw_rhs, rhs)
   46.69 -                      |> pairself (curry mk_Trueprop_eq (applied_fun_of fun_name fun_T fun_args)
   46.70 +                      |> apply2 (curry mk_Trueprop_eq (applied_fun_of fun_name fun_T fun_args)
   46.71                          #> curry Logic.list_all (map dest_Free fun_args));
   46.72                      val (distincts, discIs, _, split_sels, split_sel_asms) =
   46.73                        case_thms_of_term lthy raw_rhs;
   46.74 @@ -1372,7 +1375,7 @@
   46.75          val ctr_alists = @{map 6} (fn disc_alist => maps oooo prove_ctr disc_alist) disc_alists
   46.76            (map (map snd) sel_alists) corec_specs disc_eqnss sel_eqnss ctr_specss;
   46.77          val ctr_thmss0 = map (map snd) ctr_alists;
   46.78 -        val ctr_thmss = map (map (snd o snd) o sort (int_ord o pairself fst)) ctr_alists;
   46.79 +        val ctr_thmss = map (map (snd o snd) o sort (int_ord o apply2 fst)) ctr_alists;
   46.80  
   46.81          val code_thmss =
   46.82            @{map 6} prove_code exhaustives disc_eqnss sel_eqnss nchotomy_thmss ctr_thmss0 ctr_specss;
    47.1 --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Wed Nov 26 16:55:43 2014 +0100
    47.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Wed Nov 26 20:05:34 2014 +0100
    47.3 @@ -402,13 +402,13 @@
    47.4  
    47.5      val k = find_index (fn (_, (_, dTs, _)) => not (forall is_DtTFree dTs)) descr;
    47.6      val protoTs as (dataTs, _) = chop k descr
    47.7 -      |> (pairself o map)
    47.8 +      |> (apply2 o map)
    47.9          (fn (_, (T_name, Ds, _)) => (T_name, map (Old_Datatype_Aux.typ_of_dtyp descr) Ds));
   47.10  
   47.11      val T_names = map fst dataTs;
   47.12      val _ = eq_set (op =) (T_names, T_names0) orelse not_mutually_recursive T_names0
   47.13  
   47.14 -    val (Ts, Us) = (pairself o map) Type protoTs;
   47.15 +    val (Ts, Us) = apply2 (map Type) protoTs;
   47.16  
   47.17      val names = map Long_Name.base_name T_names;
   47.18      val (auxnames, _) = Name.make_context names
    48.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Wed Nov 26 16:55:43 2014 +0100
    48.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Wed Nov 26 20:05:34 2014 +0100
    48.3 @@ -182,7 +182,7 @@
    48.4           common_induct, induct_attrs, n2m, lthy) =
    48.5        basic_lfp_sugars_of bs arg_Ts callers callssss0 lthy0;
    48.6  
    48.7 -    val perm_basic_lfp_sugars = sort (int_ord o pairself #fp_res_index) basic_lfp_sugars;
    48.8 +    val perm_basic_lfp_sugars = sort (int_ord o apply2 #fp_res_index) basic_lfp_sugars;
    48.9  
   48.10      val indices = map #fp_res_index basic_lfp_sugars;
   48.11      val perm_indices = map #fp_res_index perm_basic_lfp_sugars;
   48.12 @@ -421,10 +421,10 @@
   48.13  
   48.14      val recs = take n_funs rec_specs |> map #recx;
   48.15      val rec_args = ctr_spec_eqn_data_list
   48.16 -      |> sort (op < o pairself (#offset o fst) |> make_ord)
   48.17 +      |> sort (op < o apply2 (#offset o fst) |> make_ord)
   48.18        |> map (uncurry (build_rec_arg ctxt funs_data has_call) o apsnd (try the_single));
   48.19      val ctr_poss = map (fn x =>
   48.20 -      if length (distinct (op = o pairself (length o #left_args)) x) <> 1 then
   48.21 +      if length (distinct (op = o apply2 (length o #left_args)) x) <> 1 then
   48.22          raise PRIMREC ("inconstant constructor pattern position for function " ^
   48.23            quote (#fun_name (hd x)), [])
   48.24        else
   48.25 @@ -480,7 +480,7 @@
   48.26      val fun_names = map Binding.name_of bs;
   48.27      val eqns_data = map (dissect_eqn lthy0 fun_names) specs;
   48.28      val funs_data = eqns_data
   48.29 -      |> partition_eq (op = o pairself #fun_name)
   48.30 +      |> partition_eq (op = o apply2 #fun_name)
   48.31        |> finds (fn (x, y) => x = #fun_name (hd y)) fun_names |> fst
   48.32        |> map (fn (x, y) => the_single y
   48.33            handle List.Empty => raise PRIMREC ("missing equations for function " ^ quote x, []));
   48.34 @@ -490,7 +490,7 @@
   48.35      val arg_Ts = map (#rec_type o hd) funs_data;
   48.36      val res_Ts = map (#res_type o hd) funs_data;
   48.37      val callssss = funs_data
   48.38 -      |> map (partition_eq (op = o pairself #ctr))
   48.39 +      |> map (partition_eq (op = o apply2 #ctr))
   48.40        |> map (maps (map_filter (find_rec_calls has_call)));
   48.41  
   48.42      fun is_only_old_datatype (Type (s, _)) =
   48.43 @@ -519,7 +519,7 @@
   48.44          : rec_spec) (fun_data : eqn_data list) =
   48.45        let
   48.46          val js =
   48.47 -          find_indices (op = o pairself (fn {fun_name, ctr, ...} => (fun_name, ctr)))
   48.48 +          find_indices (op = o apply2 (fn {fun_name, ctr, ...} => (fun_name, ctr)))
   48.49              fun_data eqns_data;
   48.50  
   48.51          val def_thms = map (snd o snd) def_thms';
    49.1 --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Wed Nov 26 16:55:43 2014 +0100
    49.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Wed Nov 26 20:05:34 2014 +0100
    49.3 @@ -362,7 +362,7 @@
    49.4        |> Local_Theory.declaration {syntax = false, pervasive = true}
    49.5          (fn phi => Data.map (fold2 (fn T_name => fn Const (size_name, _) =>
    49.6               Symtab.update (T_name, (size_name,
    49.7 -               pairself (map (Morphism.thm (phi0 $> phi))) (size_simps, flat size_gen_o_map_thmss))))
    49.8 +               apply2 (map (Morphism.thm (phi0 $> phi))) (size_simps, flat size_gen_o_map_thmss))))
    49.9             T_names size_consts))
   49.10      end
   49.11    | generate_datatype_size _ lthy = lthy;
    50.1 --- a/src/HOL/Tools/BNF/bnf_tactics.ML	Wed Nov 26 16:55:43 2014 +0100
    50.2 +++ b/src/HOL/Tools/BNF/bnf_tactics.ML	Wed Nov 26 20:05:34 2014 +0100
    50.3 @@ -51,7 +51,7 @@
    50.4  (*transforms f (g x) = h (k x) into f o g = h o k using first order matches for f, g, h, and k*)
    50.5  fun mk_pointfree ctxt thm = thm
    50.6    |> Thm.prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq
    50.7 -  |> pairself (dest_comb #> apsnd (dest_comb #> fst) #> HOLogic.mk_comp)
    50.8 +  |> apply2 (dest_comb #> apsnd (dest_comb #> fst) #> HOLogic.mk_comp)
    50.9    |> mk_Trueprop_eq
   50.10    |> (fn goal => Goal.prove_sorry ctxt [] [] goal
   50.11      (K (rtac @{thm ext} 1 THEN
    51.1 --- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Wed Nov 26 16:55:43 2014 +0100
    51.2 +++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Wed Nov 26 20:05:34 2014 +0100
    51.3 @@ -283,7 +283,7 @@
    51.4                else raise CASE_ERROR ("Wrong number of arguments for constructor " ^ quote name, i)
    51.5              else ((in_group, row :: not_in_group), names)
    51.6          | _ => raise CASE_ERROR ("Not a constructor pattern", i)))
    51.7 -    rows (([], []), replicate k "") |>> pairself rev
    51.8 +    rows (([], []), replicate k "") |>> apply2 rev
    51.9    end;
   51.10  
   51.11  
   51.12 @@ -506,7 +506,7 @@
   51.13                      (Const (s, map fastype_of xs ---> fastype_of x), p, is_dependent k t)
   51.14                    end) (constructors ~~ fs);
   51.15                  val cases' =
   51.16 -                  sort (int_ord o swap o pairself (length o snd))
   51.17 +                  sort (int_ord o swap o apply2 (length o snd))
   51.18                      (fold_rev count_cases cases []);
   51.19                  val R = fastype_of t;
   51.20                  val dummy =
    52.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Nov 26 16:55:43 2014 +0100
    52.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Nov 26 20:05:34 2014 +0100
    52.3 @@ -549,7 +549,7 @@
    52.4            val all_proto_sels = flat (@{map 3} (fn k => fn xs => map (pair k o pair xs)) ks xss xss);
    52.5            val sel_infos =
    52.6              AList.group (op =) (sel_binding_index ~~ all_proto_sels)
    52.7 -            |> sort (int_ord o pairself fst)
    52.8 +            |> sort (int_ord o apply2 fst)
    52.9              |> map snd |> curry (op ~~) uniq_sel_bindings;
   52.10            val sel_bindings = map fst sel_infos;
   52.11  
   52.12 @@ -666,7 +666,7 @@
   52.13        let
   52.14          val ((inject_thms, inject_thmss), half_distinct_thmss) = chop n thmss |>> `flat;
   52.15  
   52.16 -        val rho_As = map (pairself (certifyT lthy)) (map Logic.varifyT_global As ~~ As);
   52.17 +        val rho_As = map (apply2 (certifyT lthy)) (map Logic.varifyT_global As ~~ As);
   52.18  
   52.19          fun inst_thm t thm =
   52.20            Drule.instantiate' [] [SOME (certify lthy t)]
   52.21 @@ -717,7 +717,7 @@
   52.22            in
   52.23              (Goal.prove_sorry lthy [] [] goal (fn _ => mk_case_cong_tac lthy uexhaust_thm case_thms),
   52.24               Goal.prove_sorry lthy [] [] weak_goal (K (etac arg_cong 1)))
   52.25 -            |> pairself (singleton (Proof_Context.export names_lthy lthy) #>
   52.26 +            |> apply2 (singleton (Proof_Context.export names_lthy lthy) #>
   52.27                Thm.close_derivation)
   52.28            end;
   52.29  
    53.1 --- a/src/HOL/Tools/Function/function_common.ML	Wed Nov 26 16:55:43 2014 +0100
    53.2 +++ b/src/HOL/Tools/Function/function_common.ML	Wed Nov 26 20:05:34 2014 +0100
    53.3 @@ -177,7 +177,7 @@
    53.4  structure FunctionData = Generic_Data
    53.5  (
    53.6    type T = (term * info) Item_Net.T;
    53.7 -  val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst);
    53.8 +  val empty : T = Item_Net.init (op aconv o apply2 fst) (single o fst);
    53.9    val extend = I;
   53.10    fun merge tabs : T = Item_Net.merge tabs;
   53.11  )
    54.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Wed Nov 26 16:55:43 2014 +0100
    54.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Wed Nov 26 20:05:34 2014 +0100
    54.3 @@ -339,7 +339,7 @@
    54.4        |> (curry op COMP) wf_thm
    54.5        |> (curry op COMP) istep
    54.6  
    54.7 -    val steps_sorted = map snd (sort (int_ord o pairself fst) steps)
    54.8 +    val steps_sorted = map snd (sort (int_ord o apply2 fst) steps)
    54.9    in
   54.10      (steps_sorted, induct_rule)
   54.11    end
   54.12 @@ -356,8 +356,7 @@
   54.13      val x = Free (xn, ST)
   54.14      val cert = cterm_of (Proof_Context.theory_of ctxt)
   54.15  
   54.16 -    val ineqss = mk_ineqs R scheme
   54.17 -      |> map (map (pairself (Thm.assume o cert)))
   54.18 +    val ineqss = mk_ineqs R scheme |> map (map (apply2 (Thm.assume o cert)))
   54.19      val complete =
   54.20        map_range (mk_completeness ctxt scheme #> cert #> Thm.assume) (length branches)
   54.21      val wf_thm = mk_wf R scheme |> cert |> Thm.assume
    55.1 --- a/src/HOL/Tools/Function/pat_completeness.ML	Wed Nov 26 16:55:43 2014 +0100
    55.2 +++ b/src/HOL/Tools/Function/pat_completeness.ML	Wed Nov 26 20:05:34 2014 +0100
    55.3 @@ -26,8 +26,7 @@
    55.4  fun inst_case_thm thy x P thm =
    55.5    let val [Pv, xv] = Term.add_vars (prop_of thm) []
    55.6    in
    55.7 -    thm |> cterm_instantiate (map (pairself (cterm_of thy))
    55.8 -      [(Var xv, x), (Var Pv, P)])
    55.9 +    thm |> cterm_instantiate (map (apply2 (cterm_of thy)) [(Var xv, x), (Var Pv, P)])
   55.10    end
   55.11  
   55.12  fun invent_vars constr i =
    56.1 --- a/src/HOL/Tools/Lifting/lifting_bnf.ML	Wed Nov 26 16:55:43 2014 +0100
    56.2 +++ b/src/HOL/Tools/Lifting/lifting_bnf.ML	Wed Nov 26 20:05:34 2014 +0100
    56.3 @@ -23,7 +23,7 @@
    56.4      fun get_lhs thm = thm |> concl_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst
    56.5      val vars = get_lhs rel_Grp |> strip_comb |> snd |> map_filter (try (strip_comb #> snd #> hd))
    56.6      val UNIVs = map (fn var => HOLogic.mk_UNIV (var |> dest_Var |> snd |> dest_Type |> snd |> hd)) vars
    56.7 -    val inst = map2 (curry(pairself (certify ctxt))) vars UNIVs
    56.8 +    val inst = map2 (curry (apply2 (certify ctxt))) vars UNIVs
    56.9      val rel_Grp_UNIV_sym = rel_Grp |> Drule.instantiate_normalize ([], inst) 
   56.10        |> Local_Defs.unfold ctxt @{thms subset_UNIV[THEN eqTrueI] UNIV_def[symmetric] simp_thms(21)}
   56.11        |> (fn thm => thm RS sym)
    57.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Wed Nov 26 16:55:43 2014 +0100
    57.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Wed Nov 26 20:05:34 2014 +0100
    57.3 @@ -99,7 +99,7 @@
    57.4            end;
    57.5          
    57.6          val subst = fold make_subst free_vars [];
    57.7 -        val csubst = map (pairself (cterm_of thy)) subst;
    57.8 +        val csubst = map (apply2 (cterm_of thy)) subst;
    57.9          val inst_thm = Drule.cterm_instantiate csubst thm;
   57.10        in
   57.11          Conv.fconv_rule 
    58.1 --- a/src/HOL/Tools/Lifting/lifting_info.ML	Wed Nov 26 16:55:43 2014 +0100
    58.2 +++ b/src/HOL/Tools/Lifting/lifting_info.ML	Wed Nov 26 20:05:34 2014 +0100
    58.3 @@ -306,15 +306,16 @@
    58.4      val dest_less_eq = HOLogic.dest_bin @{const_name "less_eq"} dummyT
    58.5      val prems_pairs = map (dest_less_eq o HOLogic.dest_Trueprop) (prems_of rule)
    58.6      val equal_prems = filter op= prems_pairs
    58.7 -    val _ = if null equal_prems then () 
    58.8 +    val _ =
    58.9 +      if null equal_prems then () 
   58.10        else error "The rule contains reflexive assumptions."
   58.11      val concl_pairs = rule 
   58.12        |> concl_of
   58.13        |> HOLogic.dest_Trueprop
   58.14        |> dest_less_eq
   58.15 -      |> pairself (snd o strip_comb)
   58.16 -      |> op~~
   58.17 -      |> filter_out op=
   58.18 +      |> apply2 (snd o strip_comb)
   58.19 +      |> op ~~
   58.20 +      |> filter_out op =
   58.21      
   58.22      val _ = if has_duplicates op= concl_pairs 
   58.23        then error "The rule contains duplicated variables in the conlusion." else ()
   58.24 @@ -323,7 +324,7 @@
   58.25        if member op= concl_pairs prem_pair
   58.26        then HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm POS_def}))
   58.27        else if member op= concl_pairs (swap prem_pair)
   58.28 -        then HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm NEG_def}))
   58.29 +      then HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm NEG_def}))
   58.30        else error "The rule contains a non-relevant assumption."
   58.31      
   58.32      fun rewrite_prems [] = Conv.all_conv
    59.1 --- a/src/HOL/Tools/Meson/meson.ML	Wed Nov 26 16:55:43 2014 +0100
    59.2 +++ b/src/HOL/Tools/Meson/meson.ML	Wed Nov 26 20:05:34 2014 +0100
    59.3 @@ -109,7 +109,7 @@
    59.4            val tenv =
    59.5              Pattern.first_order_match thy (tmB, tmA)
    59.6                                            (Vartab.empty, Vartab.empty) |> snd
    59.7 -          val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
    59.8 +          val ct_pairs = map (apply2 (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
    59.9        in  thA RS (cterm_instantiate ct_pairs thB)  end) () of
   59.10      SOME th => th
   59.11    | NONE => raise THM ("first_order_resolve", 0, [thA, thB]))
   59.12 @@ -594,7 +594,7 @@
   59.13    let
   59.14      fun pat t u =
   59.15        let
   59.16 -        val ((head1, args1), (head2, args2)) = (t, u) |> pairself strip_comb
   59.17 +        val ((head1, args1), (head2, args2)) = (t, u) |> apply2 strip_comb
   59.18        in
   59.19          if head1 = head2 then
   59.20            let val pats = map2 pat args1 args2 in
   59.21 @@ -631,7 +631,7 @@
   59.22             $ (t as _ $ _) $ (u as _ $ _))) =>
   59.23      (case get_F_pattern T t u of
   59.24         SOME p =>
   59.25 -       let val inst = [pairself (cterm_of thy) (F_ext_cong_neq, p)] in
   59.26 +       let val inst = [apply2 (cterm_of thy) (F_ext_cong_neq, p)] in
   59.27           th RS cterm_instantiate inst ext_cong_neq
   59.28         end
   59.29       | NONE => th)
    60.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Wed Nov 26 16:55:43 2014 +0100
    60.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Wed Nov 26 20:05:34 2014 +0100
    60.3 @@ -375,7 +375,7 @@
    60.4                 th ctxt ctxt
    60.5      val (cnf_ths, ctxt) = clausify nnf_th
    60.6      fun intr_imp ct th =
    60.7 -      Thm.instantiate ([], map (pairself (cterm_of thy))
    60.8 +      Thm.instantiate ([], map (apply2 (cterm_of thy))
    60.9                                 [(Var (("i", 0), @{typ nat}),
   60.10                                   HOLogic.mk_nat ax_no)])
   60.11                        (zero_var_indexes @{thm skolem_COMBK_D})
    61.1 --- a/src/HOL/Tools/Metis/metis_generate.ML	Wed Nov 26 16:55:43 2014 +0100
    61.2 +++ b/src/HOL/Tools/Metis/metis_generate.ML	Wed Nov 26 20:05:34 2014 +0100
    61.3 @@ -207,7 +207,7 @@
    61.4          |> map (pair 0)
    61.5          |> Monomorph.monomorph atp_schematic_consts_of ctxt
    61.6          |> chop (length conj_clauses)
    61.7 -        |> pairself (maps (map (zero_var_indexes o snd)))
    61.8 +        |> apply2 (maps (map (zero_var_indexes o snd)))
    61.9      val num_conjs = length conj_clauses
   61.10      (* Pretend every clause is a "simp" rule, to guide the term ordering. *)
   61.11      val clauses =
    62.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Nov 26 16:55:43 2014 +0100
    62.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Nov 26 20:05:34 2014 +0100
    62.3 @@ -175,7 +175,7 @@
    62.4    let
    62.5      val tvs = Term.add_tvars (Thm.full_prop_of th) []
    62.6      val thy = Thm.theory_of_thm th
    62.7 -    fun inc_tvar ((a, i), s) = pairself (ctyp_of thy) (TVar ((a, i), s), TVar ((a, i + inc), s))
    62.8 +    fun inc_tvar ((a, i), s) = apply2 (ctyp_of thy) (TVar ((a, i), s), TVar ((a, i + inc), s))
    62.9    in
   62.10      Thm.instantiate (map inc_tvar tvs, []) th
   62.11    end
   62.12 @@ -213,7 +213,7 @@
   62.13            |> rpair (Envir.empty ~1)
   62.14            |-> fold (Pattern.unify (Context.Proof ctxt))
   62.15            |> Envir.type_env |> Vartab.dest
   62.16 -          |> map (fn (x, (S, T)) => pairself (ctyp_of thy) (TVar (x, S), T))
   62.17 +          |> map (fn (x, (S, T)) => apply2 (ctyp_of thy) (TVar (x, S), T))
   62.18        in
   62.19          (* The unifier, which is invoked from "Thm.bicompose", will sometimes refuse to unify
   62.20             "?a::?'a" with "?a::?'b" or "?a::nat" and throw a "TERM" exception (with "add_ffpair" as
   62.21 @@ -221,7 +221,7 @@
   62.22             again. We could do this the first time around but this error occurs seldom and we don't
   62.23             want to break existing proofs in subtle ways or slow them down. *)
   62.24          if null ps then raise TERM z
   62.25 -        else res (pairself (Drule.instantiate_normalize (ps, [])) (tha, thb))
   62.26 +        else res (apply2 (Drule.instantiate_normalize (ps, [])) (tha, thb))
   62.27        end
   62.28    end
   62.29  
   62.30 @@ -270,7 +270,7 @@
   62.31  
   62.32  fun resolve_inference ctxt type_enc concealed sym_tab th_pairs atom th1 th2 =
   62.33    let
   62.34 -    val (i_th1, i_th2) = pairself (lookth th_pairs) (th1, th2)
   62.35 +    val (i_th1, i_th2) = apply2 (lookth th_pairs) (th1, th2)
   62.36      val _ = trace_msg ctxt (fn () =>
   62.37          "  isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1 ^ "\n\
   62.38          \  isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
   62.39 @@ -374,7 +374,7 @@
   62.40        val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst)  (*ill-typed but gives right max*)
   62.41        val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
   62.42        val _ = trace_msg ctxt (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
   62.43 -      val eq_terms = map (pairself (cterm_of thy))
   62.44 +      val eq_terms = map (apply2 (cterm_of thy))
   62.45          (ListPair.zip (Misc_Legacy.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
   62.46    in
   62.47      cterm_instantiate eq_terms subst'
   62.48 @@ -522,7 +522,7 @@
   62.49        | _ => I)
   62.50  
   62.51      val t_inst =
   62.52 -      [] |> try (unify_terms (prem, concl) #> map (pairself (cterm_of thy)))
   62.53 +      [] |> try (unify_terms (prem, concl) #> map (apply2 (cterm_of thy)))
   62.54           |> the_default [] (* FIXME *)
   62.55    in
   62.56      cterm_instantiate t_inst th
   62.57 @@ -574,8 +574,8 @@
   62.58              Envir.Envir {maxidx = Vartab.fold (Integer.max o snd o fst) tyenv 0,
   62.59                tenv = Vartab.empty, tyenv = tyenv}
   62.60            val ty_inst =
   62.61 -            Vartab.fold (fn (x, (S, T)) => cons (pairself (ctyp_of thy) (TVar (x, S), T))) tyenv []
   62.62 -          val t_inst = [pairself (cterm_of thy o Envir.norm_term env) (Var var, t')]
   62.63 +            Vartab.fold (fn (x, (S, T)) => cons (apply2 (ctyp_of thy) (TVar (x, S), T))) tyenv []
   62.64 +          val t_inst = [apply2 (cterm_of thy o Envir.norm_term env) (Var var, t')]
   62.65          in
   62.66            Drule.instantiate_normalize (ty_inst, t_inst) th
   62.67          end
   62.68 @@ -617,7 +617,7 @@
   62.69  fun cluster_key ((ax_no, (cluster_no, index_no)), skolem) =
   62.70    (ax_no, (cluster_no, (skolem, index_no)))
   62.71  fun cluster_ord p =
   62.72 -  prod_ord int_ord (prod_ord int_ord (prod_ord bool_ord int_ord)) (pairself cluster_key p)
   62.73 +  prod_ord int_ord (prod_ord int_ord (prod_ord bool_ord int_ord)) (apply2 cluster_key p)
   62.74  
   62.75  val tysubst_ord =
   62.76    list_ord (prod_ord Term_Ord.fast_indexname_ord (prod_ord Term_Ord.sort_ord Term_Ord.typ_ord))
   62.77 @@ -630,7 +630,7 @@
   62.78    Graph(type key = int * int val ord = prod_ord int_ord int_ord)
   62.79  
   62.80  fun shuffle_key (((axiom_no, (_, index_no)), _), _) = (axiom_no, index_no)
   62.81 -fun shuffle_ord p = prod_ord int_ord int_ord (pairself shuffle_key p)
   62.82 +fun shuffle_ord p = prod_ord int_ord int_ord (apply2 shuffle_key p)
   62.83  
   62.84  (* Attempts to derive the theorem "False" from a theorem of the form
   62.85     "P1 ==> ... ==> Pn ==> False", where the "Pi"s are to be discharged using the
   62.86 @@ -651,10 +651,9 @@
   62.87              tenv |> Vartab.dest
   62.88                   |> filter (Meson_Clausify.is_zapped_var_name o fst o fst)
   62.89                   |> sort (cluster_ord
   62.90 -                          o pairself (Meson_Clausify.cluster_of_zapped_var_name
   62.91 +                          o apply2 (Meson_Clausify.cluster_of_zapped_var_name
   62.92                                        o fst o fst))
   62.93 -                 |> map (Meson.term_pair_of
   62.94 -                         #> pairself (Envir.subst_term_types tyenv))
   62.95 +                 |> map (Meson.term_pair_of #> apply2 (Envir.subst_term_types tyenv))
   62.96            val tysubst = tyenv |> Vartab.dest
   62.97          in (tysubst, tsubst) end
   62.98  
   62.99 @@ -686,7 +685,7 @@
  62.100  
  62.101        val prems = Logic.strip_imp_prems (prop_of prems_imp_false)
  62.102        val substs = prems |> map2 subst_info_of_prem (1 upto length prems)
  62.103 -                         |> sort (int_ord o pairself fst)
  62.104 +                         |> sort (int_ord o apply2 fst)
  62.105        val depss = maps (map_filter deps_of_term_subst o snd o snd o snd) substs
  62.106        val clusters = maps (op ::) depss
  62.107        val ordered_clusters =
  62.108 @@ -725,7 +724,7 @@
  62.109          "ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^
  62.110          "; tysubst: " ^ @{make_string} tysubst ^ "; tsubst: {" ^
  62.111          commas (map ((fn (s, t) => s ^ " |-> " ^ t)
  62.112 -                     o pairself (Syntax.string_of_term ctxt)) tsubst) ^ "}"
  62.113 +                     o apply2 (Syntax.string_of_term ctxt)) tsubst) ^ "}"
  62.114        val _ = tracing ("ORDERED CLUSTERS: " ^ @{make_string} ordered_clusters)
  62.115        val _ = tracing ("AXIOM COUNTS: " ^ @{make_string} ax_counts)
  62.116        val _ = tracing ("OUTER PARAMS: " ^ @{make_string} outer_param_names)
    63.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML	Wed Nov 26 16:55:43 2014 +0100
    63.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML	Wed Nov 26 20:05:34 2014 +0100
    63.3 @@ -33,7 +33,7 @@
    63.4  
    63.5  (* Designed to work also with monomorphic instances of polymorphic theorems. *)
    63.6  fun have_common_thm ths1 ths2 =
    63.7 -  exists (member (Term.aconv_untyped o pairself prop_of) ths1) (map Meson.make_meta_clause ths2)
    63.8 +  exists (member (Term.aconv_untyped o apply2 prop_of) ths1) (map Meson.make_meta_clause ths2)
    63.9  
   63.10  (*Determining which axiom clauses are actually used*)
   63.11  fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th)
   63.12 @@ -126,7 +126,7 @@
   63.13      fun weight (m, _) =
   63.14        AList.lookup (op =) ord_info (Metis_Name.toString m) |> the_default 1
   63.15      fun precedence p =
   63.16 -      (case int_ord (pairself weight p) of
   63.17 +      (case int_ord (apply2 weight p) of
   63.18          EQUAL => #precedence Metis_KnuthBendixOrder.default p
   63.19        | ord => ord)
   63.20    in {weight = weight, precedence = precedence} end
    64.1 --- a/src/HOL/Tools/Nitpick/nitpick_commands.ML	Wed Nov 26 16:55:43 2014 +0100
    64.2 +++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML	Wed Nov 26 20:05:34 2014 +0100
    64.3 @@ -187,7 +187,7 @@
    64.4             | ["", s2] => ("-" ^ s2, "-" ^ s2)
    64.5             | [s1, s2] => (s1, s2)
    64.6             | _ => raise Option.Option)
    64.7 -          |> pairself (maxed_int_from_string min_int)
    64.8 +          |> apply2 (maxed_int_from_string min_int)
    64.9        in if k1 <= k2 then k1 upto k2 else k1 downto k2 end
   64.10        handle Option.Option =>
   64.11               error ("Parameter " ^ quote name ^
    65.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Nov 26 16:55:43 2014 +0100
    65.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Nov 26 20:05:34 2014 +0100
    65.3 @@ -324,7 +324,7 @@
    65.4  
    65.5  val strip_first_name_sep =
    65.6    Substring.full #> Substring.position name_sep ##> Substring.triml 1
    65.7 -  #> pairself Substring.string
    65.8 +  #> apply2 Substring.string
    65.9  
   65.10  fun original_name s =
   65.11    if String.isPrefix nitpick_prefix s then
   65.12 @@ -460,7 +460,7 @@
   65.13    (Sign.typ_match thy (T2, T1) Vartab.empty; true)
   65.14    handle Type.TYPE_MATCH => false
   65.15  
   65.16 -fun type_match thy = strict_type_match thy o pairself unarize_unbox_etc_type
   65.17 +fun type_match thy = strict_type_match thy o apply2 unarize_unbox_etc_type
   65.18  
   65.19  fun const_match thy ((s1, T1), (s2, T2)) =
   65.20    s1 = s2 andalso type_match thy (T1, T2)
   65.21 @@ -1329,7 +1329,7 @@
   65.22    | is_ground_term _ = false
   65.23  
   65.24  fun special_bounds ts =
   65.25 -  fold Term.add_vars ts [] |> sort (Term_Ord.fast_indexname_ord o pairself fst)
   65.26 +  fold Term.add_vars ts [] |> sort (Term_Ord.fast_indexname_ord o apply2 fst)
   65.27  
   65.28  fun is_funky_typedef_name ctxt s =
   65.29    member (op =) [@{type_name unit}, @{type_name prod}, @{type_name set},
   65.30 @@ -1350,7 +1350,7 @@
   65.31      Theory.nodes_of thy
   65.32      |> maps Thm.axioms_of
   65.33      |> map (apsnd (subst_atomic subst o prop_of))
   65.34 -    |> sort (fast_string_ord o pairself fst)
   65.35 +    |> sort (fast_string_ord o apply2 fst)
   65.36      |> Ord_List.inter (fast_string_ord o apsnd fst) def_names
   65.37      |> map snd
   65.38    end
   65.39 @@ -1607,7 +1607,7 @@
   65.40                    discriminate_value hol_ctxt x (Bound 0)))
   65.41        |> AList.group (op aconv)
   65.42        |> map (apsnd (List.foldl s_disj @{const False}))
   65.43 -      |> sort (int_ord o pairself (size_of_term o snd))
   65.44 +      |> sort (int_ord o apply2 (size_of_term o snd))
   65.45        |> rev
   65.46    in
   65.47      if res_T = bool_T then
   65.48 @@ -1727,7 +1727,7 @@
   65.49          else
   65.50            do_const depth Ts t x [t1, t2, t3]
   65.51        | Const (@{const_name Let}, _) $ t1 $ t2 =>
   65.52 -        s_betapply Ts (pairself (do_term depth Ts) (t2, t1))
   65.53 +        s_betapply Ts (apply2 (do_term depth Ts) (t2, t1))
   65.54        | Const x => do_const depth Ts t x []
   65.55        | t1 $ t2 =>
   65.56          (case strip_comb t of
   65.57 @@ -1979,7 +1979,7 @@
   65.58    in
   65.59      typedef_info ctxt (fst (dest_Type abs_T)) |> the
   65.60      |> pairf #Abs_inverse #Rep_inverse
   65.61 -    |> pairself (specialize_type thy x o prop_of o the)
   65.62 +    |> apply2 (specialize_type thy x o prop_of o the)
   65.63      ||> single |> op ::
   65.64    end
   65.65  
   65.66 @@ -2089,7 +2089,7 @@
   65.67  fun wf_constraint_for rel side concl main =
   65.68    let
   65.69      val core = HOLogic.mk_mem (HOLogic.mk_prod
   65.70 -                               (pairself tuple_for_args (main, concl)), Var rel)
   65.71 +                               (apply2 tuple_for_args (main, concl)), Var rel)
   65.72      val t = List.foldl HOLogic.mk_imp core side
   65.73      val vars = filter_out (curry (op =) rel) (Term.add_vars t [])
   65.74    in
   65.75 @@ -2182,7 +2182,7 @@
   65.76      end
   65.77  
   65.78  fun num_occs_of_bound_in_term j (t1 $ t2) =
   65.79 -    op + (pairself (num_occs_of_bound_in_term j) (t1, t2))
   65.80 +    op + (apply2 (num_occs_of_bound_in_term j) (t1, t2))
   65.81    | num_occs_of_bound_in_term j (Abs (_, _, t')) =
   65.82      num_occs_of_bound_in_term (j + 1) t'
   65.83    | num_occs_of_bound_in_term j (Bound j') = if j' = j then 1 else 0
   65.84 @@ -2397,7 +2397,7 @@
   65.85              filter_out (fn (S', _) => Sign.subsort thy (S, S'))
   65.86              #> cons (S, s))
   65.87      val tfrees = [] |> fold Term.add_tfrees ts
   65.88 -                    |> sort (string_ord o pairself fst)
   65.89 +                    |> sort (string_ord o apply2 fst)
   65.90    in [] |> fold add tfrees |> rev end
   65.91  
   65.92  fun merge_type_vars_in_term thy merge_type_vars table =
    66.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Wed Nov 26 16:55:43 2014 +0100
    66.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Wed Nov 26 20:05:34 2014 +0100
    66.3 @@ -201,12 +201,12 @@
    66.4  
    66.5  fun tabulate_int_op2 debug univ_card (k, j0) f =
    66.6    tabulate_op2 debug univ_card (k, j0) j0
    66.7 -               (atom_for_int (k, 0) o f o pairself (int_for_atom (k, 0)))
    66.8 +               (atom_for_int (k, 0) o f o apply2 (int_for_atom (k, 0)))
    66.9  
   66.10  fun tabulate_int_op2_2 debug univ_card (k, j0) f =
   66.11    tabulate_op2_2 debug univ_card (k, j0) j0
   66.12 -                 (pairself (atom_for_int (k, 0)) o f
   66.13 -                  o pairself (int_for_atom (k, 0)))
   66.14 +                 (apply2 (atom_for_int (k, 0)) o f
   66.15 +                  o apply2 (int_for_atom (k, 0)))
   66.16  
   66.17  fun isa_div (m, n) = m div n handle General.Div => 0
   66.18  fun isa_mod (m, n) = m mod n handle General.Div => m
   66.19 @@ -215,7 +215,7 @@
   66.20    | isa_gcd (m, n) = isa_gcd (n, isa_mod (m, n))
   66.21  
   66.22  fun isa_lcm (m, n) = isa_div (m * n, isa_gcd (m, n))
   66.23 -val isa_zgcd = isa_gcd o pairself abs
   66.24 +val isa_zgcd = isa_gcd o apply2 abs
   66.25  
   66.26  fun isa_norm_frac (m, n) =
   66.27    if n < 0 then isa_norm_frac (~m, ~n)
   66.28 @@ -1058,7 +1058,7 @@
   66.29                if card_of_rep R1 <> 1 then
   66.30                  raise REP ("Nitpick_Kodkod.to_r (Converse)", [R])
   66.31                else
   66.32 -                pairself (Atom o pair 1 o offset_of_type ofs) (b_T, a_T)
   66.33 +                apply2 (Atom o pair 1 o offset_of_type ofs) (b_T, a_T)
   66.34              | _ => raise REP ("Nitpick_Kodkod.to_r (Converse)", [R])
   66.35            val body_R = body_rep R
   66.36            val a_arity = arity_of_rep a_R
   66.37 @@ -1163,7 +1163,7 @@
   66.38                           (fold kk_and (map_filter (fn (u, r) =>
   66.39                                if is_opt_rep (rep_of u) then SOME (kk_some r)
   66.40                                else NONE) [(u1, r1), (u2, r2)]) KK.True)
   66.41 -                         (atom_from_formula kk bool_j0 (KK.LT (pairself
   66.42 +                         (atom_from_formula kk bool_j0 (KK.LT (apply2
   66.43                               (int_expr_from_atom kk (type_of u1)) (r1, r2))))
   66.44                           KK.None)
   66.45                   (to_rep R1 u1) (to_rep R1 u2)
   66.46 @@ -1604,7 +1604,7 @@
   66.47    (delta, (epsilon, (num_binder_types T, s)))
   66.48  val constr_ord =
   66.49    prod_ord int_ord (prod_ord int_ord (prod_ord int_ord string_ord))
   66.50 -  o pairself constr_quadruple
   66.51 +  o apply2 constr_quadruple
   66.52  
   66.53  fun data_type_ord (({card = card1, self_rec = self_rec1, constrs = constr1, ...},
   66.54                      {card = card2, self_rec = self_rec2, constrs = constr2, ...})
    67.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Nov 26 16:55:43 2014 +0100
    67.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Nov 26 20:05:34 2014 +0100
    67.3 @@ -107,7 +107,7 @@
    67.4        Sign.declare_const_global ((@{binding nitpick_step}, @{typ "'a => 'a"}),
    67.5                            Mixfix (step_mixfix (), [1000], 1000)) thy
    67.6    in
    67.7 -    (pairself (pairself name_of) ((maybe_t, abs_t), (base_t, step_t)),
    67.8 +    (apply2 (apply2 name_of) ((maybe_t, abs_t), (base_t, step_t)),
    67.9       Proof_Context.transfer thy ctxt)
   67.10    end
   67.11  
   67.12 @@ -158,7 +158,7 @@
   67.13    | extract_real_number t = real (snd (HOLogic.dest_number t))
   67.14  
   67.15  fun nice_term_ord (Abs (_, _, t1), Abs (_, _, t2)) = nice_term_ord (t1, t2)
   67.16 -  | nice_term_ord tp = Real.compare (pairself extract_real_number tp)
   67.17 +  | nice_term_ord tp = Real.compare (apply2 extract_real_number tp)
   67.18      handle TERM ("dest_number", _) =>
   67.19             case tp of
   67.20               (t11 $ t12, t21 $ t22) =>
   67.21 @@ -213,7 +213,7 @@
   67.22  
   67.23  fun factor_out_types (T1 as Type (@{type_name prod}, [T11, T12]))
   67.24                       (T2 as Type (@{type_name prod}, [T21, T22])) =
   67.25 -    let val (n1, n2) = pairself num_factors_in_type (T11, T21) in
   67.26 +    let val (n1, n2) = apply2 num_factors_in_type (T11, T21) in
   67.27        if n1 = n2 then
   67.28          let
   67.29            val ((T11', opt_T12'), (T21', opt_T22')) = factor_out_types T12 T22
   67.30 @@ -259,13 +259,13 @@
   67.31            (maybe_opt, (t1 :: ts1, t2 :: ts2))
   67.32          end
   67.33        | aux t = raise TERM ("Nitpick_Model.dest_plain_fun", [t])
   67.34 -  in apsnd (pairself rev) o aux end
   67.35 +  in apsnd (apply2 rev) o aux end
   67.36  
   67.37  fun break_in_two T T1 T2 t =
   67.38    let
   67.39      val ps = HOLogic.flat_tupleT_paths T
   67.40      val cut = length (HOLogic.strip_tupleT T1)
   67.41 -    val (ps1, ps2) = pairself HOLogic.flat_tupleT_paths (T1, T2)
   67.42 +    val (ps1, ps2) = apply2 HOLogic.flat_tupleT_paths (T1, T2)
   67.43      val (ts1, ts2) = t |> HOLogic.strip_ptuple ps |> chop cut
   67.44    in (HOLogic.mk_ptuple ps1 T1 ts1, HOLogic.mk_ptuple ps2 T2 ts2) end
   67.45  
   67.46 @@ -446,7 +446,7 @@
   67.47               Type (@{type_name option}, [T2']) =>
   67.48               let
   67.49                 val (maybe_opt, ts_pair) =
   67.50 -                 dest_plain_fun t ||> pairself (map (polish_funs Ts))
   67.51 +                 dest_plain_fun t ||> apply2 (map (polish_funs Ts))
   67.52               in make_map maybe_opt T1 T2 T2' (rev (op ~~ ts_pair)) end
   67.53             | _ => raise SAME ()
   67.54           else
   67.55 @@ -472,7 +472,7 @@
   67.56               | t => t
   67.57      fun make_fun_or_set maybe_opt T T1 T2 T' ts1 ts2 =
   67.58        ts1 ~~ ts2
   67.59 -      |> sort (nice_term_ord o pairself fst)
   67.60 +      |> sort (nice_term_ord o apply2 fst)
   67.61        |> (case T of
   67.62              Type (@{type_name set}, _) =>
   67.63              sort_wrt (truth_const_sort_key o snd)
   67.64 @@ -703,7 +703,7 @@
   67.65  fun intersect_formats _ [] = []
   67.66    | intersect_formats [] _ = []
   67.67    | intersect_formats ks1 ks2 =
   67.68 -    let val ((ks1', k1), (ks2', k2)) = pairself split_last (ks1, ks2) in
   67.69 +    let val ((ks1', k1), (ks2', k2)) = apply2 split_last (ks1, ks2) in
   67.70        intersect_formats (ks1' @ (if k1 > k2 then [k1 - k2] else []))
   67.71                          (ks2' @ (if k2 > k1 then [k2 - k1] else [])) @
   67.72        [Int.min (k1, k2)]
   67.73 @@ -870,7 +870,7 @@
   67.74        if exists_subtype (member (op =) coTs) T then
   67.75          let
   67.76            val ((head1, args1), (head2, args2)) =
   67.77 -            pairself (strip_comb o unfold_outer_the_binders) (t1, t2)
   67.78 +            apply2 (strip_comb o unfold_outer_the_binders) (t1, t2)
   67.79            val max_depth = max_depth - (if member (op =) coTs T then 1 else 0)
   67.80          in
   67.81            head1 = head2 andalso
    68.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Wed Nov 26 16:55:43 2014 +0100
    68.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Wed Nov 26 20:05:34 2014 +0100
    68.3 @@ -161,7 +161,7 @@
    68.4    | repair_mtype cache seen (MFun (M1, aa, M2)) =
    68.5      MFun (repair_mtype cache seen M1, aa, repair_mtype cache seen M2)
    68.6    | repair_mtype cache seen (MPair Mp) =
    68.7 -    MPair (pairself (repair_mtype cache seen) Mp)
    68.8 +    MPair (apply2 (repair_mtype cache seen) Mp)
    68.9    | repair_mtype cache seen (MType (s, Ms)) =
   68.10      MType (s, maps (flatten_mtype o repair_mtype cache seen) Ms)
   68.11    | repair_mtype cache seen (MRec (z as (s, _))) =
   68.12 @@ -228,7 +228,7 @@
   68.13        else case T of
   68.14          Type (@{type_name fun}, [T1, T2]) =>
   68.15          MFun (fresh_mfun_for_fun_type mdata all_minus T1 T2)
   68.16 -      | Type (@{type_name prod}, [T1, T2]) => MPair (pairself do_type (T1, T2))
   68.17 +      | Type (@{type_name prod}, [T1, T2]) => MPair (apply2 do_type (T1, T2))
   68.18        | Type (@{type_name set}, [T']) => do_type (T' --> bool_T)
   68.19        | Type (z as (s, _)) =>
   68.20          if could_exist_alpha_sub_mtype ctxt alpha_T T then
   68.21 @@ -320,7 +320,7 @@
   68.22      fun aux MAlpha = MAlpha
   68.23        | aux (MFun (M1, aa, M2)) =
   68.24          MFun (aux M1, resolve_annotation_atom asgs aa, aux M2)
   68.25 -      | aux (MPair Mp) = MPair (pairself aux Mp)
   68.26 +      | aux (MPair Mp) = MPair (apply2 aux Mp)
   68.27        | aux (MType (s, Ms)) = MType (s, map aux Ms)
   68.28        | aux (MRec z) = MRec z
   68.29    in aux end
   68.30 @@ -506,8 +506,8 @@
   68.31  fun prop_for_atom_equality (aa1, A a2) = prop_for_atom_assign (aa1, a2)
   68.32    | prop_for_atom_equality (A a1, aa2) = prop_for_atom_assign (aa2, a1)
   68.33    | prop_for_atom_equality (V x1, V x2) =
   68.34 -    Prop_Logic.SAnd (prop_for_bool_var_equality (pairself fst_var (x1, x2)),
   68.35 -             prop_for_bool_var_equality (pairself snd_var (x1, x2)))
   68.36 +    Prop_Logic.SAnd (prop_for_bool_var_equality (apply2 fst_var (x1, x2)),
   68.37 +             prop_for_bool_var_equality (apply2 snd_var (x1, x2)))
   68.38  
   68.39  val prop_for_assign_clause = Prop_Logic.exists o map prop_for_assign_literal
   68.40  
   68.41 @@ -530,9 +530,9 @@
   68.42    fold (fn x => fn accum =>
   68.43             if AList.defined (op =) asgs x then
   68.44               accum
   68.45 -           else case (fst_var x, snd_var x) |> pairself assigns of
   68.46 +           else case (fst_var x, snd_var x) |> apply2 assigns of
   68.47               (NONE, NONE) => accum
   68.48 -           | bp => (x, annotation_from_bools (pairself (the_default false) bp))
   68.49 +           | bp => (x, annotation_from_bools (apply2 (the_default false) bp))
   68.50                     :: accum)
   68.51         (max_var downto 1) asgs
   68.52  
    69.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Wed Nov 26 16:55:43 2014 +0100
    69.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Wed Nov 26 20:05:34 2014 +0100
    69.3 @@ -765,7 +765,7 @@
    69.4        else if is_Cst True u2 then u1
    69.5        else raise SAME ()
    69.6      | Eq =>
    69.7 -      (case pairself (is_Cst Unrep) (u1, u2) of
    69.8 +      (case apply2 (is_Cst Unrep) (u1, u2) of
    69.9           (true, true) => unknown_boolean T R
   69.10         | (false, false) => raise SAME ()
   69.11         | _ => if forall (is_opt_rep o rep_of) [u1, u2] then raise SAME ()
    70.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Nov 26 16:55:43 2014 +0100
    70.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Nov 26 20:05:34 2014 +0100
    70.3 @@ -173,10 +173,9 @@
    70.4        end
    70.5      and do_equals new_Ts old_Ts s0 T0 t1 t2 =
    70.6        let
    70.7 -        val (t1, t2) = pairself (do_term new_Ts old_Ts Neut) (t1, t2)
    70.8 -        val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2)
    70.9 -        val T = if def then T1
   70.10 -                else [T1, T2] |> sort (int_ord o pairself size_of_typ) |> hd
   70.11 +        val (t1, t2) = apply2 (do_term new_Ts old_Ts Neut) (t1, t2)
   70.12 +        val (T1, T2) = apply2 (curry fastype_of1 new_Ts) (t1, t2)
   70.13 +        val T = if def then T1 else [T1, T2] |> sort (int_ord o apply2 size_of_typ) |> hd
   70.14        in
   70.15          list_comb (Const (s0, T --> T --> body_type T0),
   70.16                     map2 (coerce_term hol_ctxt new_Ts T) [T1, T2] [t1, t2])
   70.17 @@ -608,9 +607,9 @@
   70.18          | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
   70.19            do_quantifier s0 T0 s1 T1 t1
   70.20          | @{const HOL.conj} $ t1 $ t2 =>
   70.21 -          s_conj (pairself (aux ss Ts js skolemizable polar) (t1, t2))
   70.22 +          s_conj (apply2 (aux ss Ts js skolemizable polar) (t1, t2))
   70.23          | @{const HOL.disj} $ t1 $ t2 =>
   70.24 -          s_disj (pairself (aux ss Ts js skolemizable polar) (t1, t2))
   70.25 +          s_disj (apply2 (aux ss Ts js skolemizable polar) (t1, t2))
   70.26          | @{const HOL.implies} $ t1 $ t2 =>
   70.27            @{const HOL.implies} $ aux ss Ts js skolemizable (flip_polarity polar) t1
   70.28            $ aux ss Ts js skolemizable polar t2
   70.29 @@ -758,7 +757,7 @@
   70.30                  val _ = not (null fixed_js) orelse raise SAME ()
   70.31                  val fixed_args = filter_indices fixed_js args
   70.32                  val vars = fold Term.add_vars fixed_args []
   70.33 -                           |> sort (Term_Ord.fast_indexname_ord o pairself fst)
   70.34 +                           |> sort (Term_Ord.fast_indexname_ord o apply2 fst)
   70.35                  val bound_js = fold (fn t => fn js => add_loose_bnos (t, 0, js))
   70.36                                      fixed_args []
   70.37                                 |> sort int_ord
   70.38 @@ -811,11 +810,11 @@
   70.39  
   70.40  fun special_congruence_axiom T (js1, ts1, x1) (js2, ts2, x2) =
   70.41    let
   70.42 -    val (bounds1, bounds2) = pairself (map Var o special_bounds) (ts1, ts2)
   70.43 +    val (bounds1, bounds2) = apply2 (map Var o special_bounds) (ts1, ts2)
   70.44      val Ts = binder_types T
   70.45      val max_j = fold (fold Integer.max) [js1, js2] ~1
   70.46      val (eqs, (args1, args2)) =
   70.47 -      fold (fn j => case pairself (fn ps => AList.lookup (op =) ps j)
   70.48 +      fold (fn j => case apply2 (fn ps => AList.lookup (op =) ps j)
   70.49                                    (js1 ~~ ts1, js2 ~~ ts2) of
   70.50                        (SOME t1, SOME t2) => apfst (cons (t1, t2))
   70.51                      | (SOME t1, NONE) => apsnd (apsnd (cons t1))
   70.52 @@ -823,7 +822,7 @@
   70.53                      | (NONE, NONE) =>
   70.54                        let val v = Var ((cong_var_prefix ^ nat_subscript j, 0),
   70.55                                         nth Ts j) in
   70.56 -                        apsnd (pairself (cons v))
   70.57 +                        apsnd (apply2 (cons v))
   70.58                        end) (max_j downto 0) ([], ([], []))
   70.59    in
   70.60      Logic.list_implies (eqs |> filter_out (op aconv) |> distinct (op =)
   70.61 @@ -849,7 +848,7 @@
   70.62        | do_pass_1 T skipped _ [] = do_pass_2 T skipped
   70.63        | do_pass_1 T skipped all (z :: zs) =
   70.64          case filter (is_more_specific z) all
   70.65 -             |> sort (int_ord o pairself generality) of
   70.66 +             |> sort (int_ord o apply2 generality) of
   70.67            [] => do_pass_1 T (z :: skipped) all zs
   70.68          | (z' :: _) => cons (special_congruence_axiom T z z')
   70.69                         #> do_pass_1 T skipped all zs
   70.70 @@ -883,7 +882,7 @@
   70.71  fun all_table_entries table = Symtab.fold (append o snd) table []
   70.72  
   70.73  fun extra_table tables s =
   70.74 -  Symtab.make [(s, pairself all_table_entries tables |> op @)]
   70.75 +  Symtab.make [(s, apply2 all_table_entries tables |> op @)]
   70.76  
   70.77  fun eval_axiom_for_term j t =
   70.78    Logic.mk_equals (Const (eval_prefix ^ string_of_int j, fastype_of t), t)
   70.79 @@ -1199,7 +1198,7 @@
   70.80                           val (costly_boundss, (j, js)) =
   70.81                             js |> map (`(merge costly_boundss o single))
   70.82                                |> sort (int_ord
   70.83 -                                       o pairself (Integer.sum o map snd o fst))
   70.84 +                                       o apply2 (Integer.sum o map snd o fst))
   70.85                                |> split_list |>> hd ||> pairf hd tl
   70.86                         in
   70.87                           j :: heuristically_best_permutation costly_boundss js
   70.88 @@ -1208,7 +1207,7 @@
   70.89                       if length Ts <= quantifier_cluster_threshold then
   70.90                         all_permutations (index_seq 0 num_Ts)
   70.91                         |> map (`(cost (t_boundss ~~ t_costs)))
   70.92 -                       |> sort (int_ord o pairself fst) |> hd |> snd
   70.93 +                       |> sort (int_ord o apply2 fst) |> hd |> snd
   70.94                       else
   70.95                         heuristically_best_permutation (t_boundss ~~ t_costs)
   70.96                                                        (index_seq 0 num_Ts)
    71.1 --- a/src/HOL/Tools/Nitpick/nitpick_rep.ML	Wed Nov 26 16:55:43 2014 +0100
    71.2 +++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML	Wed Nov 26 20:05:34 2014 +0100
    71.3 @@ -213,7 +213,7 @@
    71.4    | min_rep (Struct Rs) _ = Struct Rs
    71.5    | min_rep _ (Struct Rs) = Struct Rs
    71.6    | min_rep (R1 as Func (R11, R12)) (R2 as Func (R21, R22)) =
    71.7 -    (case pairself is_opt_rep (R12, R22) of
    71.8 +    (case apply2 is_opt_rep (R12, R22) of
    71.9         (true, false) => R1
   71.10       | (false, true) => R2
   71.11       | _ => if R11 = R21 then Func (R11, min_rep R12 R22)
    72.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Wed Nov 26 16:55:43 2014 +0100
    72.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Wed Nov 26 20:05:34 2014 +0100
    72.3 @@ -214,7 +214,7 @@
    72.4    #data_types s1 = #data_types s2 andalso #card_assigns s1 = #card_assigns s2
    72.5  
    72.6  fun scope_less_eq (s1 : scope) (s2 : scope) =
    72.7 -  (s1, s2) |> pairself (map snd o #card_assigns) |> op ~~ |> forall (op <=)
    72.8 +  (s1, s2) |> apply2 (map snd o #card_assigns) |> op ~~ |> forall (op <=)
    72.9  
   72.10  fun rank_of_row (_, ks) = length ks
   72.11  
   72.12 @@ -293,7 +293,7 @@
   72.13            k :: ks |> map (fn k => (k + linearity) * (k + linearity))
   72.14                    |> Integer.sum
   72.15    in
   72.16 -    all_combinations #> map (`cost) #> sort (int_ord o pairself fst) #> map snd
   72.17 +    all_combinations #> map (`cost) #> sort (int_ord o apply2 fst) #> map snd
   72.18    end
   72.19  
   72.20  fun is_self_recursive_constr_type T =
   72.21 @@ -449,7 +449,7 @@
   72.22      val xs = binarized_and_boxed_data_type_constrs hol_ctxt binarize T
   72.23      val self_recs = map (is_self_recursive_constr_type o snd) xs
   72.24      val (num_self_recs, num_non_self_recs) =
   72.25 -      List.partition I self_recs |> pairself length
   72.26 +      List.partition I self_recs |> apply2 length
   72.27      val self_rec = num_self_recs > 0
   72.28      fun is_complete facto =
   72.29        has_exact_card hol_ctxt facto finitizable_dataTs card_assigns T
   72.30 @@ -467,7 +467,7 @@
   72.31      val constrs =
   72.32        fold_rev (add_constr_spec desc (not co) card sum_dom_cards num_self_recs
   72.33                                  num_non_self_recs)
   72.34 -               (sort (bool_ord o swap o pairself fst) (self_recs ~~ xs)) []
   72.35 +               (sort (bool_ord o swap o apply2 fst) (self_recs ~~ xs)) []
   72.36    in
   72.37      {typ = T, card = card, co = co, self_rec = self_rec, complete = complete,
   72.38       concrete = concrete, deep = deep, constrs = constrs}
    73.1 --- a/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML	Wed Nov 26 16:55:43 2014 +0100
    73.2 +++ b/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML	Wed Nov 26 20:05:34 2014 +0100
    73.3 @@ -396,7 +396,7 @@
    73.4      fun max xs = fold max_inf xs (SOME 0);
    73.5      val (_, _, constrs) = the (AList.lookup (op =) descr i);
    73.6      val xs =
    73.7 -      sort (int_ord o pairself snd)
    73.8 +      sort (int_ord o apply2 snd)
    73.9          (map_filter (fn (s, dts) => Option.map (pair s)
   73.10            (max (map (arg_nonempty o strip_dtyp) dts))) constrs)
   73.11    in if null xs then NONE else SOME (hd xs) end;
    74.1 --- a/src/HOL/Tools/Old_Datatype/old_datatype_data.ML	Wed Nov 26 16:55:43 2014 +0100
    74.2 +++ b/src/HOL/Tools/Old_Datatype/old_datatype_data.ML	Wed Nov 26 20:05:34 2014 +0100
    74.3 @@ -162,7 +162,7 @@
    74.4      val k = find_index (fn (_, (_, dTs, _)) => not (forall is_DtTFree dTs)) descr;
    74.5      val protoTs as (dataTs, _) =
    74.6        chop k descr
    74.7 -      |> (pairself o map)
    74.8 +      |> (apply2 o map)
    74.9          (fn (_, (tyco, dTs, _)) => (tyco, map (Old_Datatype_Aux.typ_of_dtyp descr) dTs));
   74.10  
   74.11      val tycos = map fst dataTs;
   74.12 @@ -172,7 +172,7 @@
   74.13          error ("Type constructors " ^ commas_quote raw_tycos ^
   74.14            " do not belong exhaustively to one mutually recursive old-style datatype");
   74.15  
   74.16 -    val (Ts, Us) = (pairself o map) Type protoTs;
   74.17 +    val (Ts, Us) = apply2 (map Type) protoTs;
   74.18  
   74.19      val names = map Long_Name.base_name tycos;
   74.20      val (auxnames, _) =
    75.1 --- a/src/HOL/Tools/Predicate_Compile/core_data.ML	Wed Nov 26 16:55:43 2014 +0100
    75.2 +++ b/src/HOL/Tools/Predicate_Compile/core_data.ML	Wed Nov 26 20:05:34 2014 +0100
    75.3 @@ -234,7 +234,7 @@
    75.4        let
    75.5          fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t)
    75.6          fun inst_of_matches tts = fold (Pattern.match thy) tts (Vartab.empty, Vartab.empty)
    75.7 -          |> snd |> Vartab.dest |> map (pairself (cterm_of thy) o term_pair_of)
    75.8 +          |> snd |> Vartab.dest |> map (apply2 (cterm_of thy) o term_pair_of)
    75.9          val (cases, (eqs, prems)) = apsnd (chop (nargs - nparams)) (chop n prems)
   75.10          val case_th =
   75.11            rewrite_rule ctxt (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1))
   75.12 @@ -445,8 +445,8 @@
   75.13    let
   75.14      (* thm refl is a dummy thm *)
   75.15      val modes = map fst compilations
   75.16 -    val (needs_random, non_random_modes) = pairself (map fst)
   75.17 -      (List.partition (fn (_, (_, random)) => random) compilations)
   75.18 +    val (needs_random, non_random_modes) =
   75.19 +      apply2 (map fst) (List.partition (fn (_, (_, random)) => random) compilations)
   75.20      val non_random_dummys = map (rpair "dummy") non_random_modes
   75.21      val all_dummys = map (rpair "dummy") modes
   75.22      val dummy_function_names =
    76.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Nov 26 16:55:43 2014 +0100
    76.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Nov 26 20:05:34 2014 +0100
    76.3 @@ -350,7 +350,7 @@
    76.4          else if eq_mode (m, Output) then (NONE,  SOME t)
    76.5          else raise Fail "split_map_mode: mode and term do not match"
    76.6    in
    76.7 -    (pairself (map_filter I) o split_list) (map2 split_arg_mode' (strip_fun_mode mode) ts)
    76.8 +    (apply2 (map_filter I) o split_list) (map2 split_arg_mode' (strip_fun_mode mode) ts)
    76.9    end
   76.10  
   76.11  (* splits mode and maps function to higher-order argument types *)
   76.12 @@ -368,7 +368,7 @@
   76.13        | split_arg_mode' Output T = (NONE,  SOME T)
   76.14        | split_arg_mode' _ _ = raise Fail "split_modeT': mode and type do not match"
   76.15    in
   76.16 -    (pairself (map_filter I) o split_list) (map2 split_arg_mode' (strip_fun_mode mode) Ts)
   76.17 +    (apply2 (map_filter I) o split_list) (map2 split_arg_mode' (strip_fun_mode mode) Ts)
   76.18    end
   76.19  
   76.20  fun split_mode mode ts = split_map_mode (fn _ => fn _ => (NONE, NONE)) mode ts
   76.21 @@ -400,7 +400,7 @@
   76.22        | split_arg_mode Output T = ([], [T])
   76.23        | split_arg_mode _ _ = raise Fail "split_modeT: mode and type do not match"
   76.24    in
   76.25 -    (pairself flat o split_list) (map2 split_arg_mode (strip_fun_mode mode) Ts)
   76.26 +    (apply2 flat o split_list) (map2 split_arg_mode (strip_fun_mode mode) Ts)
   76.27    end
   76.28  
   76.29  fun string_of_mode mode =
    77.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Nov 26 16:55:43 2014 +0100
    77.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Nov 26 20:05:34 2014 +0100
    77.3 @@ -210,7 +210,7 @@
    77.4        | check _ _ = false
    77.5      fun check_consistent_modes ms =
    77.6        if forall (fn Fun _ => true | _ => false) ms then
    77.7 -        pairself check_consistent_modes (split_list (map (fn Fun (m1, m2) => (m1, m2)) ms))
    77.8 +        apply2 check_consistent_modes (split_list (map (fn Fun (m1, m2) => (m1, m2)) ms))
    77.9          |> (fn (res1, res2) => res1 andalso res2)
   77.10        else if forall (fn Input => true | Output => true | Pair _ => true | _ => false) ms then
   77.11          true
   77.12 @@ -864,7 +864,7 @@
   77.13    let
   77.14      fun select_best_switch moded_clauses input_position best_switch =
   77.15        let
   77.16 -        val ord = option_ord (rev_order o int_ord o (pairself (length o snd o snd)))
   77.17 +        val ord = option_ord (rev_order o int_ord o (apply2 (length o snd o snd)))
   77.18          val partition = partition_clause ctxt input_position moded_clauses
   77.19          val switch = if (length (fst partition) > 1) then SOME (input_position, partition) else NONE
   77.20        in
    78.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Wed Nov 26 16:55:43 2014 +0100
    78.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Wed Nov 26 20:05:34 2014 +0100
    78.3 @@ -21,7 +21,7 @@
    78.4  structure Fun_Pred = Theory_Data
    78.5  (
    78.6    type T = (term * term) Item_Net.T;
    78.7 -  val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst);
    78.8 +  val empty : T = Item_Net.init (op aconv o apply2 fst) (single o fst);
    78.9    val extend = I;
   78.10    val merge = Item_Net.merge;
   78.11  )
   78.12 @@ -295,7 +295,7 @@
   78.13            map Drule.export_without_context (filter (Predicate_Compile_Aux.is_intro predname) intrs)))
   78.14          dst_prednames
   78.15        val thy'' = Fun_Pred.map
   78.16 -        (fold Item_Net.update (map (pairself Logic.varify_global)
   78.17 +        (fold Item_Net.update (map (apply2 Logic.varify_global)
   78.18            (dst_funs ~~ dst_preds))) thy'
   78.19        fun functional_mode_of T =
   78.20          list_fun_mode (replicate (length (binder_types T)) Input @ [Output])
    79.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Wed Nov 26 16:55:43 2014 +0100
    79.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Wed Nov 26 20:05:34 2014 +0100
    79.3 @@ -19,7 +19,7 @@
    79.4  structure Specialisations = Theory_Data
    79.5  (
    79.6    type T = (term * term) Item_Net.T
    79.7 -  val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst)
    79.8 +  val empty : T = Item_Net.init (op aconv o apply2 fst) (single o fst)
    79.9    val extend = I
   79.10    val merge = Item_Net.merge
   79.11  )
   79.12 @@ -49,7 +49,7 @@
   79.13          (Var _, []) => (true, true)
   79.14        | (Free _, []) => (true, true)
   79.15        | (Const (@{const_name Pair}, _), ts) =>
   79.16 -        pairself (forall I) (split_list (map check ts))
   79.17 +        apply2 (forall I) (split_list (map check ts))
   79.18        | (Const (s, T), ts) =>
   79.19            (case (AList.lookup (op =) cnstrs s, body_type T) of
   79.20              (SOME (i, Tname), Type (Tname', _)) => (false,
    80.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Wed Nov 26 16:55:43 2014 +0100
    80.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Wed Nov 26 20:05:34 2014 +0100
    80.3 @@ -694,7 +694,7 @@
    80.4  val (_, oracle) = Context.>>> (Context.map_theory_result
    80.5    (Thm.add_oracle (@{binding cooper},
    80.6      (fn (ctxt, t) =>
    80.7 -      (Thm.cterm_of (Proof_Context.theory_of ctxt) o Logic.mk_equals o pairself HOLogic.mk_Trueprop)
    80.8 +      (Thm.cterm_of (Proof_Context.theory_of ctxt) o Logic.mk_equals o apply2 HOLogic.mk_Trueprop)
    80.9          (t, procedure t)))));
   80.10  
   80.11  val comp_ss =
    81.1 --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Wed Nov 26 16:55:43 2014 +0100
    81.2 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Wed Nov 26 20:05:34 2014 +0100
    81.3 @@ -417,7 +417,7 @@
    81.4      else case perhaps_constrain thy insts vs
    81.5       of SOME constrain => instantiate config descr
    81.6            (map constrain vs) tycos prfx (names, auxnames)
    81.7 -            ((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
    81.8 +            ((apply2 o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
    81.9        | NONE => thy
   81.10    end;
   81.11  
   81.12 @@ -491,7 +491,7 @@
   81.13        Type (@{type_name fun}, [T1, T2]) =>
   81.14          (case try dest_fun_upds t of
   81.15            SOME (tps, t) =>
   81.16 -            (map (pairself post_process_term) tps, map_Abs post_process_term t)
   81.17 +            (map (apply2 post_process_term) tps, map_Abs post_process_term t)
   81.18              |> (case T2 of
   81.19                @{typ bool} => 
   81.20                  (case t of
    82.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Wed Nov 26 16:55:43 2014 +0100
    82.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Wed Nov 26 20:05:34 2014 +0100
    82.3 @@ -171,7 +171,7 @@
    82.4      if has_all_vars vs (Thm.term_of ct) then
    82.5        (case Thm.term_of ct of
    82.6          _ $ _ =>
    82.7 -          (case pairself (minimal_pats vs) (Thm.dest_comb ct) of
    82.8 +          (case apply2 (minimal_pats vs) (Thm.dest_comb ct) of
    82.9              ([], []) => [[ct]]
   82.10            | (ctss, ctss') => union (eq_set (op aconvc)) ctss ctss')
   82.11        | _ => [])
   82.12 @@ -189,7 +189,7 @@
   82.13    fun mk_pat ct = Thm.apply (SMT_Util.instT' ct pat) ct
   82.14  
   82.15    fun mk_clist T =
   82.16 -    pairself (Thm.cterm_of @{theory}) (SMT_Util.symb_cons_const T, SMT_Util.symb_nil_const T)
   82.17 +    apply2 (Thm.cterm_of @{theory}) (SMT_Util.symb_cons_const T, SMT_Util.symb_nil_const T)
   82.18    fun mk_list (ccons, cnil) f cts = fold_rev (Thm.mk_binop ccons o f) cts cnil
   82.19    val mk_pat_list = mk_list (mk_clist @{typ pattern})
   82.20    val mk_mpat_list = mk_list (mk_clist @{typ "pattern symb_list"})
    83.1 --- a/src/HOL/Tools/SMT/smtlib_interface.ML	Wed Nov 26 16:55:43 2014 +0100
    83.2 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Wed Nov 26 20:05:34 2014 +0100
    83.3 @@ -149,7 +149,7 @@
    83.4      |> fold (Buffer.add o enclose "(declare-sort " " 0)\n") (sort fast_string_ord sorts)
    83.5      |> fold sdtyp (AList.coalesce (op =) dtyps)
    83.6      |> fold (Buffer.add o enclose "(declare-fun " ")\n" o string_of_fun)
    83.7 -        (sort (fast_string_ord o pairself fst) funcs)
    83.8 +        (sort (fast_string_ord o apply2 fst) funcs)
    83.9      |> fold (fn (i, t) => Buffer.add (enclose "(assert " ")\n"
   83.10          (SMTLIB.str_of (named_sterm (assert_name_of_index i) (tree_of_sterm 0 t))))) (map_index I ts)
   83.11      |> Buffer.add "(check-sat)\n"
    84.1 --- a/src/HOL/Tools/SMT/z3_proof.ML	Wed Nov 26 16:55:43 2014 +0100
    84.2 +++ b/src/HOL/Tools/SMT/z3_proof.ML	Wed Nov 26 20:05:34 2014 +0100
    84.3 @@ -221,7 +221,7 @@
    84.4  fun with_quant pred i (Const q1 $ Abs (_, T1, t1), Const q2 $ Abs (_, T2, t2)) =
    84.5        if pred q1 q2 andalso T1 = T2 then
    84.6          let val t = Var (("", i), T1)
    84.7 -        in SOME (pairself Term.subst_bound ((t, t1), (t, t2))) end
    84.8 +        in SOME (apply2 Term.subst_bound ((t, t1), (t, t2))) end
    84.9        else NONE
   84.10    | with_quant _ _ _ = NONE
   84.11  
    85.1 --- a/src/HOL/Tools/SMT/z3_replay_literals.ML	Wed Nov 26 16:55:43 2014 +0100
    85.2 +++ b/src/HOL/Tools/SMT/z3_replay_literals.ML	Wed Nov 26 20:05:34 2014 +0100
    85.3 @@ -254,7 +254,7 @@
    85.4        | NONE =>
    85.5            (case lookup_rule t of
    85.6              (rewrite, SOME lit) => (s, rewrite lit)
    85.7 -          | (_, NONE) => (s, comp (pairself join1 (dest t)))))
    85.8 +          | (_, NONE) => (s, comp (apply2 join1 (dest t)))))
    85.9  
   85.10    in snd (join1 (if is_conj then (false, t) else (true, t))) end
   85.11  
   85.12 @@ -289,7 +289,7 @@
   85.13          SOME rs => extract_lit thm rs
   85.14        | NONE =>
   85.15            the (Termtab.get_first contra_lits rules)
   85.16 -          |> pairself (extract_lit thm)
   85.17 +          |> apply2 (extract_lit thm)
   85.18            |> (fn (nlit, plit) => nlit COMP (plit COMP contra_rule)))
   85.19      end
   85.20  
    86.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Nov 26 16:55:43 2014 +0100
    86.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Nov 26 20:05:34 2014 +0100
    86.3 @@ -82,7 +82,7 @@
    86.4            (used_facts,
    86.5             (case AList.lookup (op =) ress preferred_meth of
    86.6               SOME play => (preferred_meth, play)
    86.7 -           | NONE => hd (sort (play_outcome_ord o pairself snd) (rev ress))))
    86.8 +           | NONE => hd (sort (play_outcome_ord o apply2 snd) (rev ress))))
    86.9          | try_methss ress (meths :: methss) =
   86.10            let
   86.11              fun mk_step fact_names meths =
    87.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Nov 26 16:55:43 2014 +0100
    87.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Nov 26 20:05:34 2014 +0100
    87.3 @@ -348,7 +348,7 @@
    87.4    | normalize_eq t = t
    87.5  
    87.6  fun if_thm_before th th' =
    87.7 -  if Theory.subthy (pairself Thm.theory_of_thm (th, th')) then th else th'
    87.8 +  if Theory.subthy (apply2 Thm.theory_of_thm (th, th')) then th else th'
    87.9  
   87.10  (* Hack: Conflate the facts about a class as seen from the outside with the corresponding low-level
   87.11     facts, so that MaSh can learn from the low-level proofs. *)
   87.12 @@ -373,7 +373,7 @@
   87.13  
   87.14  fun fact_distinct eq facts =
   87.15    fold (fn fact as (_, th) =>
   87.16 -      Net.insert_term_safe (eq o pairself (normalize_eq o prop_of o snd))
   87.17 +      Net.insert_term_safe (eq o apply2 (normalize_eq o prop_of o snd))
   87.18          (normalize_eq (prop_of th), fact))
   87.19      facts Net.empty
   87.20    |> Net.entries
   87.21 @@ -542,7 +542,7 @@
   87.22             o fact_of_ref ctxt keywords chained css) add
   87.23         else
   87.24           let
   87.25 -           val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del)
   87.26 +           val (add, del) = apply2 (Attrib.eval_thms ctxt) (add, del)
   87.27             val facts =
   87.28               all_facts ctxt false ho_atp keywords add chained css
   87.29               |> filter_out ((member Thm.eq_thm_prop del orf
    88.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML	Wed Nov 26 16:55:43 2014 +0100
    88.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML	Wed Nov 26 20:05:34 2014 +0100
    88.3 @@ -145,7 +145,7 @@
    88.4      val (typing_spots, tvar_count_tab) =
    88.5        Var_Set_Tab.fold (fn kv as (k, _) => apfst (cons kv) #> apsnd (update_count 1 k))
    88.6          typing_spot_tab ([], Vartab.empty)
    88.7 -      |>> sort_distinct (rev_order o cost_ord o pairself snd)
    88.8 +      |>> sort_distinct (rev_order o cost_ord o apply2 snd)
    88.9    in
   88.10      fold drop_superfluous typing_spots ([], tvar_count_tab) |> fst
   88.11    end
    89.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Wed Nov 26 16:55:43 2014 +0100
    89.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Wed Nov 26 20:05:34 2014 +0100
    89.3 @@ -195,7 +195,7 @@
    89.4          let
    89.5            val cand_key = apfst (length o get_successors)
    89.6            val cand_ord =
    89.7 -            prod_ord int_ord (prod_ord (int_ord o swap) (int_ord o swap)) o pairself cand_key
    89.8 +            prod_ord int_ord (prod_ord (int_ord o swap) (int_ord o swap)) o apply2 cand_key
    89.9  
   89.10            fun pop_next_candidate [] = (NONE, [])
   89.11              | pop_next_candidate (cands as (cand :: cands')) =
    90.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Wed Nov 26 16:55:43 2014 +0100
    90.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Wed Nov 26 20:05:34 2014 +0100
    90.3 @@ -104,7 +104,7 @@
    90.4  fun resolve_fact_names ctxt names =
    90.5    (names
    90.6     |>> map string_of_label
    90.7 -   |> pairself (maps (thms_of_name ctxt)))
    90.8 +   |> apply2 (maps (thms_of_name ctxt)))
    90.9    handle ERROR msg => error ("preplay error: " ^ msg)
   90.10  
   90.11  fun thm_of_proof ctxt (Proof (fixed_frees, assms, steps)) =
   90.12 @@ -176,7 +176,7 @@
   90.13      val meths = proof_methods_of_isar_step step |> subtract (op =) hopeless
   90.14    in
   90.15      par_list_map_filter_with_timeout get_time min_preplay_timeout timeout0 preplay meths
   90.16 -    |> sort (play_outcome_ord o pairself snd)
   90.17 +    |> sort (play_outcome_ord o apply2 snd)
   90.18    end
   90.19  
   90.20  type isar_preplay_data = (proof_method * play_outcome Lazy.lazy) list Canonical_Label_Tab.table
   90.21 @@ -188,7 +188,7 @@
   90.22    | add_preplay_outcomes _ Play_Failed = Play_Failed
   90.23    | add_preplay_outcomes (Played time1) (Played time2) = Played (Time.+ (time1, time2))
   90.24    | add_preplay_outcomes play1 play2 =
   90.25 -    Play_Timed_Out (Time.+ (pairself time_of_play (play1, play2)))
   90.26 +    Play_Timed_Out (Time.+ (apply2 time_of_play (play1, play2)))
   90.27  
   90.28  fun set_preplay_outcomes_of_isar_step ctxt timeout preplay_data
   90.29        (step as Prove (_, _, l, _, _, _, meths, _)) meths_outcomes0 =
   90.30 @@ -207,7 +207,7 @@
   90.31  fun get_best_method_outcome force =
   90.32    tap (List.app (K () o Lazy.future Future.default_params o snd)) (* could be parallelized *)
   90.33    #> map (apsnd force)
   90.34 -  #> sort (play_outcome_ord o pairself snd)
   90.35 +  #> sort (play_outcome_ord o apply2 snd)
   90.36    #> hd
   90.37  
   90.38  fun forced_intermediate_preplay_outcome_of_isar_step preplay_data l =
    91.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Wed Nov 26 16:55:43 2014 +0100
    91.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Wed Nov 26 20:05:34 2014 +0100
    91.3 @@ -81,7 +81,7 @@
    91.4  val have_prefix = "f"
    91.5  
    91.6  fun label_ord ((s1, i1), (s2, i2)) =
    91.7 -  (case int_ord (pairself String.size (s1, s2)) of
    91.8 +  (case int_ord (apply2 String.size (s1, s2)) of
    91.9      EQUAL =>
   91.10      (case string_ord (s1, s2) of
   91.11        EQUAL => int_ord (i1, i2)
    92.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Nov 26 16:55:43 2014 +0100
    92.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Nov 26 20:05:34 2014 +0100
    92.3 @@ -187,7 +187,7 @@
    92.4        fun weight_of fact = mess |> map_filter (score_in fact) |> scaled_avg
    92.5      in
    92.6        fold (union fact_eq o map fst o take max_facts o fst o snd) mess []
    92.7 -      |> map (`weight_of) |> sort (int_ord o pairself fst o swap)
    92.8 +      |> map (`weight_of) |> sort (int_ord o apply2 fst o swap)
    92.9        |> map snd |> take max_facts
   92.10      end
   92.11  
   92.12 @@ -363,7 +363,7 @@
   92.13        if at = num_facts then acc else ret (at + 1) (Array.sub (posterior, at) :: acc)
   92.14    in
   92.15      select_visible_facts 100000.0 posterior visible_facts;
   92.16 -    sort_array_suffix (Real.compare o pairself snd) max_suggs posterior;
   92.17 +    sort_array_suffix (Real.compare o apply2 snd) max_suggs posterior;
   92.18      ret (Integer.max 0 (num_facts - max_suggs)) []
   92.19    end
   92.20  
   92.21 @@ -396,7 +396,7 @@
   92.22        end
   92.23  
   92.24      val _ = List.app do_feat goal_feats
   92.25 -    val _ = sort_array_suffix (Real.compare o pairself snd) num_facts overlaps_sqr
   92.26 +    val _ = sort_array_suffix (Real.compare o apply2 snd) num_facts overlaps_sqr
   92.27      val no_recommends = Unsynchronized.ref 0
   92.28      val recommends = Array.tabulate (num_facts, rpair 0.0)
   92.29      val age = Unsynchronized.ref 500000000.0
   92.30 @@ -438,7 +438,7 @@
   92.31      while1 ();
   92.32      while2 ();
   92.33      select_visible_facts 1000000000.0 recommends visible_facts;
   92.34 -    sort_array_suffix (Real.compare o pairself snd) max_suggs recommends;
   92.35 +    sort_array_suffix (Real.compare o apply2 snd) max_suggs recommends;
   92.36      ret [] (Integer.max 0 (num_facts - max_suggs))
   92.37    end
   92.38  
   92.39 @@ -777,24 +777,24 @@
   92.40    else if Theory.subthy (swap p) then
   92.41      GREATER
   92.42    else
   92.43 -    (case int_ord (pairself (length o Theory.ancestors_of) p) of
   92.44 -      EQUAL => string_ord (pairself Context.theory_name p)
   92.45 +    (case int_ord (apply2 (length o Theory.ancestors_of) p) of
   92.46 +      EQUAL => string_ord (apply2 Context.theory_name p)
   92.47      | order => order)
   92.48  
   92.49  fun crude_thm_ord p =
   92.50 -  (case crude_theory_ord (pairself theory_of_thm p) of
   92.51 +  (case crude_theory_ord (apply2 theory_of_thm p) of
   92.52      EQUAL =>
   92.53      (* The hack below is necessary because of odd dependencies that are not reflected in the theory
   92.54         comparison. *)
   92.55 -    let val q = pairself nickname_of_thm p in
   92.56 +    let val q = apply2 nickname_of_thm p in
   92.57        (* Hack to put "xxx_def" before "xxxI" and "xxxE" *)
   92.58 -      (case bool_ord (pairself (String.isSuffix "_def") (swap q)) of
   92.59 +      (case bool_ord (apply2 (String.isSuffix "_def") (swap q)) of
   92.60          EQUAL => string_ord q
   92.61        | ord => ord)
   92.62      end
   92.63    | ord => ord)
   92.64  
   92.65 -val thm_less_eq = Theory.subthy o pairself theory_of_thm
   92.66 +val thm_less_eq = Theory.subthy o apply2 theory_of_thm
   92.67  fun thm_less p = thm_less_eq p andalso not (thm_less_eq (swap p))
   92.68  
   92.69  val freezeT = Type.legacy_freeze_type
   92.70 @@ -1154,7 +1154,7 @@
   92.71      val algorithm = the_mash_algorithm ()
   92.72  
   92.73      val facts = facts
   92.74 -      |> rev_sort_list_prefix (crude_thm_ord o pairself snd)
   92.75 +      |> rev_sort_list_prefix (crude_thm_ord o apply2 snd)
   92.76          (Int.max (num_extra_feature_facts, max_proximity_facts))
   92.77  
   92.78      val chained = filter (fn ((_, (scope, _)), _) => scope = Chained) facts
   92.79 @@ -1184,7 +1184,7 @@
   92.80  
   92.81      val goal_feats =
   92.82        fold (union (eq_fst (op =))) [chained_feats, extra_feats] (map (rpair 1.0) goal_feats0)
   92.83 -      |> debug ? sort (Real.compare o swap o pairself snd)
   92.84 +      |> debug ? sort (Real.compare o swap o apply2 snd)
   92.85  
   92.86      val parents = maximal_wrt_access_graph access_G facts
   92.87      val visible_facts = map_filter (Symtab.lookup fact_tab) (Graph.all_preds access_G parents)
   92.88 @@ -1209,7 +1209,7 @@
   92.89      val unknown = filter_out (is_fact_in_graph access_G o snd) facts
   92.90    in
   92.91      find_mash_suggestions ctxt max_suggs suggs facts chained unknown
   92.92 -    |> pairself (map fact_of_raw_fact)
   92.93 +    |> apply2 (map fact_of_raw_fact)
   92.94    end
   92.95  
   92.96  fun mash_unlearn () = (clear_state (); writeln "Reset MaSh.")
   92.97 @@ -1268,7 +1268,7 @@
   92.98        let
   92.99          val thy = Proof_Context.theory_of ctxt
  92.100          val feats = features_of ctxt thy (Local, General) [t]
  92.101 -        val facts = rev_sort_list_prefix (crude_thm_ord o pairself snd) 1 facts
  92.102 +        val facts = rev_sort_list_prefix (crude_thm_ord o apply2 snd) 1 facts
  92.103        in
  92.104          map_state ctxt
  92.105            (fn {access_G, xtabs as ((num_facts0, _), _), ffds, freqs, dirty_facts} =>
  92.106 @@ -1397,7 +1397,7 @@
  92.107            else
  92.108              let
  92.109                val new_facts = facts
  92.110 -                |> sort (crude_thm_ord o pairself snd)
  92.111 +                |> sort (crude_thm_ord o apply2 snd)
  92.112                  |> attach_parents_to_facts []
  92.113                  |> filter_out (is_in_access_G o snd)
  92.114                val (learns, (num_nontrivial, _, _)) =
  92.115 @@ -1444,7 +1444,7 @@
  92.116                val old_facts = facts
  92.117                  |> filter is_in_access_G
  92.118                  |> map (`(priority_of o snd))
  92.119 -                |> sort (int_ord o pairself fst)
  92.120 +                |> sort (int_ord o apply2 fst)
  92.121                  |> map snd
  92.122                val ((relearns, flops), (num_nontrivial, _, _)) =
  92.123                  (([], []), (num_nontrivial, next_commit_time (), false))
  92.124 @@ -1469,7 +1469,7 @@
  92.125      val ctxt = ctxt |> Config.put instantiate_inducts false
  92.126      val facts =
  92.127        nearly_all_facts ctxt false fact_override Keyword.empty_keywords css chained [] @{prop True}
  92.128 -      |> sort (crude_thm_ord o pairself snd o swap)
  92.129 +      |> sort (crude_thm_ord o apply2 snd o swap)
  92.130      val num_facts = length facts
  92.131      val prover = hd provers
  92.132  
    93.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Wed Nov 26 16:55:43 2014 +0100
    93.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Wed Nov 26 20:05:34 2014 +0100
    93.3 @@ -361,7 +361,7 @@
    93.4        Real.ceil (Math.pow (max_imperfect,
    93.5          Math.pow (Real.fromInt remaining_max / Real.fromInt max_facts, max_imperfect_exp)))
    93.6      val (perfect, imperfect) = candidates
    93.7 -      |> sort (Real.compare o swap o pairself snd)
    93.8 +      |> sort (Real.compare o swap o apply2 snd)
    93.9        |> take_prefix (fn (_, w) => w > 0.99999)
   93.10      val ((accepts, more_rejects), rejects) =
   93.11        chop max_imperfect imperfect |>> append perfect |>> chop remaining_max
    94.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Wed Nov 26 16:55:43 2014 +0100
    94.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Wed Nov 26 20:05:34 2014 +0100
    94.3 @@ -149,11 +149,11 @@
    94.4    | string_of_play_outcome Play_Failed = "failed"
    94.5  
    94.6  fun play_outcome_ord (Played time1, Played time2) =
    94.7 -    int_ord (pairself Time.toMilliseconds (time1, time2))
    94.8 +    int_ord (apply2 Time.toMilliseconds (time1, time2))
    94.9    | play_outcome_ord (Played _, _) = LESS
   94.10    | play_outcome_ord (_, Played _) = GREATER
   94.11    | play_outcome_ord (Play_Timed_Out time1, Play_Timed_Out time2) =
   94.12 -    int_ord (pairself Time.toMilliseconds (time1, time2))
   94.13 +    int_ord (apply2 Time.toMilliseconds (time1, time2))
   94.14    | play_outcome_ord (Play_Timed_Out _, _) = LESS
   94.15    | play_outcome_ord (_, Play_Timed_Out _) = GREATER
   94.16    | play_outcome_ord (Play_Failed, Play_Failed) = EQUAL
    95.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Wed Nov 26 16:55:43 2014 +0100
    95.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Wed Nov 26 20:05:34 2014 +0100
    95.3 @@ -178,7 +178,7 @@
    95.4              | _ =>
    95.5                let
    95.6                  val (sup_r0, (l, result)) = min depth result (sup @ r0) l0
    95.7 -                val (sup, r0) = (sup, r0) |> pairself (filter_used_facts true (map fst sup_r0))
    95.8 +                val (sup, r0) = (sup, r0) |> apply2 (filter_used_facts true (map fst sup_r0))
    95.9                  val (sup_l, (r, result)) = min depth result (sup @ l) r0
   95.10                  val sup = sup |> filter_used_facts true (map fst sup_l)
   95.11                in (sup, (l @ r, result)) end))
    96.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Nov 26 16:55:43 2014 +0100
    96.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Nov 26 20:05:34 2014 +0100
    96.3 @@ -115,7 +115,7 @@
    96.4    (case try Thm.proof_body_of th of
    96.5      NONE => NONE
    96.6    | SOME body =>
    96.7 -    let val map_names = (case name_tabs of SOME p => pairself Symtab.lookup p | NONE => `I SOME) in
    96.8 +    let val map_names = (case name_tabs of SOME p => apply2 Symtab.lookup p | NONE => `I SOME) in
    96.9        SOME (fold_body_thm max_thms (Thm.get_name_hint th) map_names (Proofterm.strip_thm body))
   96.10        handle TOO_MANY () => NONE
   96.11      end)
    97.1 --- a/src/HOL/Tools/TFL/rules.ML	Wed Nov 26 16:55:43 2014 +0100
    97.2 +++ b/src/HOL/Tools/TFL/rules.ML	Wed Nov 26 20:05:34 2014 +0100
    97.3 @@ -389,7 +389,7 @@
    97.4  fun IT_EXISTS blist th =
    97.5     let val thy = Thm.theory_of_thm th
    97.6         val tych = cterm_of thy
    97.7 -       val blist' = map (pairself Thm.term_of) blist
    97.8 +       val blist' = map (apply2 Thm.term_of) blist
    97.9         fun ex v M  = cterm_of thy (USyntax.mk_exists{Bvar=v,Body = M})
   97.10  
   97.11    in
    98.1 --- a/src/HOL/Tools/TFL/tfl.ML	Wed Nov 26 16:55:43 2014 +0100
    98.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Wed Nov 26 20:05:34 2014 +0100
    98.3 @@ -333,7 +333,7 @@
    98.4                                      {path=[a], rows=rows}
    98.5       val patts1 = map (fn (_,tag,[pat]) => (pat,tag)) patts
    98.6            handle Match => mk_functional_err "error in pattern-match translation"
    98.7 -     val patts2 = Library.sort (Library.int_ord o Library.pairself row_of_pat) patts1
    98.8 +     val patts2 = Library.sort (Library.int_ord o apply2 row_of_pat) patts1
    98.9       val finals = map row_of_pat patts2
   98.10       val originals = map (row_of_pat o #2) rows
   98.11       val dummy = case (subtract (op =) finals originals)
    99.1 --- a/src/HOL/Tools/Transfer/transfer.ML	Wed Nov 26 16:55:43 2014 +0100
    99.2 +++ b/src/HOL/Tools/Transfer/transfer.ML	Wed Nov 26 20:05:34 2014 +0100
    99.3 @@ -48,7 +48,7 @@
    99.4  
    99.5  (** Theory Data **)
    99.6  
    99.7 -val compound_xhs_empty_net = Item_Net.init (Thm.eq_thm_prop o pairself snd) (single o fst);
    99.8 +val compound_xhs_empty_net = Item_Net.init (Thm.eq_thm_prop o apply2 snd) (single o fst);
    99.9  val rewr_rules = Item_Net.init Thm.eq_thm_prop (single o fst o HOLogic.dest_eq
   99.10    o HOLogic.dest_Trueprop o Thm.concl_of);
   99.11  
   100.1 --- a/src/HOL/Tools/code_evaluation.ML	Wed Nov 26 16:55:43 2014 +0100
   100.2 +++ b/src/HOL/Tools/code_evaluation.ML	Wed Nov 26 20:05:34 2014 +0100
   100.3 @@ -62,7 +62,7 @@
   100.4      val t = list_comb (Const (c, tys ---> ty),
   100.5        map Free (Name.invent_names Name.context "a" tys));
   100.6      val (arg, rhs) =
   100.7 -      pairself (Thm.cterm_of thy o Logic.unvarify_types_global o Logic.varify_global)
   100.8 +      apply2 (Thm.cterm_of thy o Logic.unvarify_types_global o Logic.varify_global)
   100.9          (t,
  100.10            map_aterms (fn t as Free (_, ty) => HOLogic.mk_term_of ty t | t => t)
  100.11              (HOLogic.reflect_term t));
   101.1 --- a/src/HOL/Tools/coinduction.ML	Wed Nov 26 16:55:43 2014 +0100
   101.2 +++ b/src/HOL/Tools/coinduction.ML	Wed Nov 26 20:05:34 2014 +0100
   101.3 @@ -65,8 +65,8 @@
   101.4              |> fold Variable.declare_thm (raw_thm :: prems);
   101.5            val thm_concl = Thm.cprop_of raw_thm |> strip_imp_concl;
   101.6            val (rhoTs, rhots) = Thm.match (thm_concl, concl)
   101.7 -            |>> map (pairself typ_of)
   101.8 -            ||> map (pairself term_of);
   101.9 +            |>> map (apply2 typ_of)
  101.10 +            ||> map (apply2 term_of);
  101.11            val xs = hd (Thm.prems_of raw_thm) |> HOLogic.dest_Trueprop |> strip_comb |> snd
  101.12              |> map (subst_atomic_types rhoTs);
  101.13            val raw_eqs = map (fn x => (x, AList.lookup op aconv rhots x |> the)) xs;
   102.1 --- a/src/HOL/Tools/datatype_realizer.ML	Wed Nov 26 16:55:43 2014 +0100
   102.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Wed Nov 26 20:05:34 2014 +0100
   102.3 @@ -106,7 +106,7 @@
   102.4          (map (fn ((((i, _), T), U), tname) =>
   102.5            make_pred i U T (mk_proj i is r) (Free (tname, T)))
   102.6              (descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
   102.7 -    val inst = map (pairself cert) (map head_of (HOLogic.dest_conj
   102.8 +    val inst = map (apply2 cert) (map head_of (HOLogic.dest_conj
   102.9        (HOLogic.dest_Trueprop (concl_of induct))) ~~ ps);
  102.10  
  102.11      val thm =
   103.1 --- a/src/HOL/Tools/functor.ML	Wed Nov 26 16:55:43 2014 +0100
   103.2 +++ b/src/HOL/Tools/functor.ML	Wed Nov 26 20:05:34 2014 +0100
   103.3 @@ -149,8 +149,8 @@
   103.4      val lhs1 = list_comb (head, map (HOLogic.id_const) arg_Ts);
   103.5      val lhs2 = list_comb (head, map (fn arg_T => Abs ("x", arg_T, Bound 0)) arg_Ts);
   103.6      val rhs = HOLogic.id_const T;
   103.7 -    val (id_prop, identity_prop) = pairself
   103.8 -      (HOLogic.mk_Trueprop o HOLogic.mk_eq o rpair rhs) (lhs1, lhs2);
   103.9 +    val (id_prop, identity_prop) =
  103.10 +      apply2 (HOLogic.mk_Trueprop o HOLogic.mk_eq o rpair rhs) (lhs1, lhs2);
  103.11      fun prove_identity ctxt id_thm = Goal.prove_sorry ctxt [] [] identity_prop
  103.12        (K (ALLGOALS (Method.insert_tac [id_thm] THEN'
  103.13          Simplifier.asm_lr_simp_tac (put_simpset identity_ss ctxt))));
  103.14 @@ -206,11 +206,12 @@
  103.15      fun bad_typ () = error ("Bad mapper type: " ^ Syntax.string_of_typ ctxt T);
  103.16      val (Ts, T1, T2) = split_mapper_typ tyco T
  103.17        handle List.Empty => bad_typ ();
  103.18 -    val _ = pairself
  103.19 -      ((fn tyco' => if tyco' = tyco then () else bad_typ ()) o fst o dest_Type) (T1, T2)
  103.20 -      handle TYPE _ => bad_typ ();
  103.21 -    val (vs1, vs2) = pairself (map dest_TFree o snd o dest_Type) (T1, T2)
  103.22 -      handle TYPE _ => bad_typ ();
  103.23 +    val _ =
  103.24 +      apply2 ((fn tyco' => if tyco' = tyco then () else bad_typ ()) o fst o dest_Type) (T1, T2)
  103.25 +        handle TYPE _ => bad_typ ();
  103.26 +    val (vs1, vs2) =
  103.27 +      apply2 (map dest_TFree o snd o dest_Type) (T1, T2)
  103.28 +        handle TYPE _ => bad_typ ();
  103.29      val _ = if has_duplicates (eq_fst (op =)) (vs1 @ vs2)
  103.30        then bad_typ () else ();
  103.31      fun check_variance_pair (var1 as (_, sort1), var2 as (_, sort2)) =
  103.32 @@ -239,7 +240,7 @@
  103.33        let
  103.34          val typ_instance = Sign.typ_instance (Context.theory_of context);
  103.35          val mapper' = Morphism.term phi mapper;
  103.36 -        val T_T' = pairself fastype_of (mapper, mapper');
  103.37 +        val T_T' = apply2 fastype_of (mapper, mapper');
  103.38          val vars = Term.add_vars mapper' [];
  103.39        in
  103.40          if null vars andalso typ_instance T_T' andalso typ_instance (swap T_T')
   104.1 --- a/src/HOL/Tools/hologic.ML	Wed Nov 26 16:55:43 2014 +0100
   104.2 +++ b/src/HOL/Tools/hologic.ML	Wed Nov 26 20:05:34 2014 +0100
   104.3 @@ -205,7 +205,7 @@
   104.4  
   104.5  fun conj_intr thP thQ =
   104.6    let
   104.7 -    val (P, Q) = pairself (Object_Logic.dest_judgment o Thm.cprop_of) (thP, thQ)
   104.8 +    val (P, Q) = apply2 (Object_Logic.dest_judgment o Thm.cprop_of) (thP, thQ)
   104.9        handle CTERM (msg, _) => raise THM (msg, 0, [thP, thQ]);
  104.10      val inst = Thm.instantiate ([], [(@{cpat "?P::bool"}, P), (@{cpat "?Q::bool"}, Q)]);
  104.11    in Drule.implies_elim_list (inst @{thm conjI}) [thP, thQ] end;
   105.1 --- a/src/HOL/Tools/inductive_realizer.ML	Wed Nov 26 16:55:43 2014 +0100
   105.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Wed Nov 26 20:05:34 2014 +0100
   105.3 @@ -262,7 +262,7 @@
   105.4      val vs1 = map Var (filter_out (fn ((a, _), _) => member (op =) rvs a) xs);
   105.5      val rlzvs = rev (Term.add_vars (prop_of rrule) []);
   105.6      val vs2 = map (fn (ixn, _) => Var (ixn, (the o AList.lookup (op =) rlzvs) ixn)) xs;
   105.7 -    val rs = map Var (subtract (op = o pairself fst) xs rlzvs);
   105.8 +    val rs = map Var (subtract (op = o apply2 fst) xs rlzvs);
   105.9      val rlz' = fold_rev Logic.all rs (prop_of rrule)
  105.10    in (name, (vs,
  105.11      if rt = Extraction.nullt then rt else fold_rev lambda vs1 rt,
  105.12 @@ -340,7 +340,7 @@
  105.13            val s' = Long_Name.base_name s;
  105.14            val T' = Logic.unvarifyT_global T;
  105.15          in (((s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end)
  105.16 -      |> distinct (op = o pairself (#1 o #1))
  105.17 +      |> distinct (op = o apply2 (#1 o #1))
  105.18        |> map (apfst (apfst (apfst Binding.name)))
  105.19        |> split_list;
  105.20  
  105.21 @@ -369,7 +369,7 @@
  105.22  
  105.23      fun add_ind_realizer Ps thy =
  105.24        let
  105.25 -        val vs' = rename (map (pairself (fst o fst o dest_Var))
  105.26 +        val vs' = rename (map (apply2 (fst o fst o dest_Var))
  105.27            (params ~~ List.take (snd (strip_comb (HOLogic.dest_Trueprop
  105.28              (hd (prems_of (hd inducts))))), nparms))) vs;
  105.29          val rs = indrule_realizer thy induct raw_induct rsets params'
  105.30 @@ -491,7 +491,7 @@
  105.31    let
  105.32      val (_, {intrs, induct, raw_induct, elims, ...}) =
  105.33        Inductive.the_inductive (Proof_Context.init_global thy) name;
  105.34 -    val vss = sort (int_ord o pairself length)
  105.35 +    val vss = sort (int_ord o apply2 length)
  105.36        (subsets (map fst (relevant_vars (concl_of (hd intrs)))))
  105.37    in
  105.38      fold_rev (add_ind_realizer rsets intrs induct raw_induct elims) vss thy
   106.1 --- a/src/HOL/Tools/lin_arith.ML	Wed Nov 26 16:55:43 2014 +0100
   106.2 +++ b/src/HOL/Tools/lin_arith.ML	Wed Nov 26 20:05:34 2014 +0100
   106.3 @@ -317,10 +317,9 @@
   106.4            new
   106.5        | NONE     =>
   106.6            (case t of Abs (a, T, body) =>
   106.7 -            let val pairs' = map (pairself (incr_boundvars 1)) pairs
   106.8 +            let val pairs' = map (apply2 (incr_boundvars 1)) pairs
   106.9              in  Abs (a, T, subst_term pairs' body)  end
  106.10 -          | t1 $ t2                   =>
  106.11 -            subst_term pairs t1 $ subst_term pairs t2
  106.12 +          | t1 $ t2 => subst_term pairs t1 $ subst_term pairs t2
  106.13            | _ => t));
  106.14  
  106.15  (* approximates the effect of one application of split_tac (followed by NNF  *)
   107.1 --- a/src/HOL/Tools/monomorph.ML	Wed Nov 26 16:55:43 2014 +0100
   107.2 +++ b/src/HOL/Tools/monomorph.ML	Wed Nov 26 20:05:34 2014 +0100
   107.3 @@ -159,7 +159,7 @@
   107.4  
   107.5  fun instantiate thy subst =
   107.6    let
   107.7 -    fun cert (ix, (S, T)) = pairself (Thm.ctyp_of thy) (TVar (ix, S), T)
   107.8 +    fun cert (ix, (S, T)) = apply2 (Thm.ctyp_of thy) (TVar (ix, S), T)
   107.9      fun cert' subst = Vartab.fold (cons o cert) subst []
  107.10    in Thm.instantiate (cert' subst, []) end
  107.11  
  107.12 @@ -287,15 +287,15 @@
  107.13  fun size_of_subst subst =
  107.14    Vartab.fold (Integer.add o size_of_typ o snd o snd) subst 0
  107.15  
  107.16 -fun subst_ord subst = int_ord (pairself size_of_subst subst)
  107.17 +fun subst_ord subst = int_ord (apply2 size_of_subst subst)
  107.18  
  107.19  fun instantiated_thms _ _ (Ground thm) = [(0, thm)]
  107.20    | instantiated_thms _ _ Ignored = []
  107.21    | instantiated_thms max_thm_insts insts (Schematic {id, ...}) =
  107.22      Inttab.lookup_list insts id
  107.23 -    |> (fn rthms => if length rthms <= max_thm_insts then rthms
  107.24 -      else take max_thm_insts
  107.25 -        (sort (prod_ord int_ord subst_ord o pairself fst) rthms))
  107.26 +    |> (fn rthms =>
  107.27 +      if length rthms <= max_thm_insts then rthms
  107.28 +      else take max_thm_insts (sort (prod_ord int_ord subst_ord o apply2 fst) rthms))
  107.29      |> map (apfst fst)
  107.30  
  107.31  fun monomorph schematic_consts_of ctxt rthms =
   108.1 --- a/src/HOL/Tools/record.ML	Wed Nov 26 16:55:43 2014 +0100
   108.2 +++ b/src/HOL/Tools/record.ML	Wed Nov 26 20:05:34 2014 +0100
   108.3 @@ -1475,7 +1475,7 @@
   108.4        | [x] => (head_of x, false));
   108.5      val rule'' =
   108.6        cterm_instantiate
   108.7 -        (map (pairself cert)
   108.8 +        (map (apply2 cert)
   108.9            (case rev params of
  108.10              [] =>
  108.11                (case AList.lookup (op =) (Term.add_frees g []) s of
  108.12 @@ -1758,7 +1758,7 @@
  108.13        fun mk_eq_refl thy =
  108.14          @{thm equal_refl}
  108.15          |> Thm.instantiate
  108.16 -          ([pairself (ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], [])
  108.17 +          ([apply2 (ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], [])
  108.18          |> Axclass.unoverload thy;
  108.19        val ensure_random_record = ensure_sort_record (@{sort random}, mk_random_eq);
  108.20        val ensure_exhaustive_record =
   109.1 --- a/src/HOL/Tools/reification.ML	Wed Nov 26 16:55:43 2014 +0100
   109.2 +++ b/src/HOL/Tools/reification.ML	Wed Nov 26 20:05:34 2014 +0100
   109.3 @@ -231,7 +231,7 @@
   109.4          val substt =
   109.5            let
   109.6              val ih = Drule.cterm_rule (Thm.instantiate (subst_ty, []));
   109.7 -          in map (pairself ih) (subst_ns @ subst_vs @ cts) end;
   109.8 +          in map (apply2 ih) (subst_ns @ subst_vs @ cts) end;
   109.9          val th = (Drule.instantiate_normalize (subst_ty, substt) eq) RS sym;
  109.10        in (hd (Variable.export ctxt'' ctxt [th]), bds) end)
  109.11        handle Pattern.MATCH => tryeqs eqs (ct, ctxt) bds);
  109.12 @@ -279,7 +279,8 @@
  109.13    let
  109.14      val (congs, bds) = mk_congs ctxt eqs;
  109.15      val congs = rearrange congs;
  109.16 -    val (th, bds') = apfst mk_eq (divide_and_conquer' (decomp_reify (mk_decompatom eqs) congs) (ct, ctxt) bds);
  109.17 +    val (th, bds') =
  109.18 +      apfst mk_eq (divide_and_conquer' (decomp_reify (mk_decompatom eqs) congs) (ct, ctxt) bds);
  109.19      fun is_list_var (Var (_, t)) = can dest_listT t
  109.20        | is_list_var _ = false;
  109.21      val vars = th |> prop_of |> Logic.dest_equals |> snd
  109.22 @@ -287,7 +288,7 @@
  109.23      val cert = cterm_of (Proof_Context.theory_of ctxt);
  109.24      val vs = map (fn v as Var (_, T) =>
  109.25        (v, the (AList.lookup Type.could_unify bds' T) |> snd |> HOLogic.mk_list (dest_listT T))) vars;
  109.26 -    val th' = Drule.instantiate_normalize ([], (map o pairself) cert vs) th;
  109.27 +    val th' = Drule.instantiate_normalize ([], (map o apply2) cert vs) th;
  109.28      val th'' = Thm.symmetric (dereify ctxt [] (Thm.lhs_of th'));
  109.29    in Thm.transitive th'' th' end;
  109.30  
   110.1 --- a/src/HOL/Tools/rewrite_hol_proof.ML	Wed Nov 26 16:55:43 2014 +0100
   110.2 +++ b/src/HOL/Tools/rewrite_hol_proof.ML	Wed Nov 26 20:05:34 2014 +0100
   110.3 @@ -13,7 +13,7 @@
   110.4  structure RewriteHOLProof : REWRITE_HOL_PROOF =
   110.5  struct
   110.6  
   110.7 -val rews = map (pairself (Proof_Syntax.proof_of_term @{theory} true) o
   110.8 +val rews = map (apply2 (Proof_Syntax.proof_of_term @{theory} true) o
   110.9      Logic.dest_equals o Logic.varify_global o Proof_Syntax.read_term @{theory} true propT)
  110.10  
  110.11    (** eliminate meta-equality rules **)
   111.1 --- a/src/HOL/Tools/sat.ML	Wed Nov 26 16:55:43 2014 +0100
   111.2 +++ b/src/HOL/Tools/sat.ML	Wed Nov 26 20:05:34 2014 +0100
   111.3 @@ -128,7 +128,7 @@
   111.4          fun merge xs [] = xs
   111.5            | merge [] ys = ys
   111.6            | merge (x :: xs) (y :: ys) =
   111.7 -              (case (lit_ord o pairself fst) (x, y) of
   111.8 +              (case lit_ord (apply2 fst (x, y)) of
   111.9                  LESS => x :: merge xs (y :: ys)
  111.10                | EQUAL => x :: merge xs ys
  111.11                | GREATER => y :: merge (x :: xs) ys)
  111.12 @@ -139,7 +139,7 @@
  111.13            | find_res_hyps (_, []) _ =
  111.14                raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
  111.15            | find_res_hyps (h1 :: hyps1, h2 :: hyps2) acc =
  111.16 -              (case (lit_ord o pairself fst) (h1, h2) of
  111.17 +              (case lit_ord  (apply2 fst (h1, h2)) of
  111.18                  LESS  => find_res_hyps (hyps1, h2 :: hyps2) (h1 :: acc)
  111.19                | EQUAL =>
  111.20                    let
  111.21 @@ -227,7 +227,7 @@
  111.22            let
  111.23              val _ = cond_tracing ctxt (fn () => "Using original clause #" ^ string_of_int id)
  111.24              val raw = CNF.clause2raw_thm thm
  111.25 -            val hyps = sort (lit_ord o pairself fst) (map_filter (fn chyp =>
  111.26 +            val hyps = sort (lit_ord o apply2 fst) (map_filter (fn chyp =>
  111.27                Option.map (rpair chyp) (index_of_literal chyp)) (#hyps (Thm.crep_thm raw)))
  111.28              val clause = (raw, hyps)
  111.29              val _ = Array.update (clauses, id, RAW_CLAUSE clause)
  111.30 @@ -304,7 +304,7 @@
  111.31      (* Conjunction.intr_balanced and fold Thm.weaken below, is quadratic for *)
  111.32      (* terms sorted in descending order, while only linear for terms      *)
  111.33      (* sorted in ascending order                                          *)
  111.34 -    val sorted_clauses = sort (Term_Ord.fast_term_ord o pairself Thm.term_of) nontrivial_clauses
  111.35 +    val sorted_clauses = sort (Term_Ord.fast_term_ord o apply2 Thm.term_of) nontrivial_clauses
  111.36      val _ =
  111.37        cond_tracing ctxt (fn () =>
  111.38          "Sorted non-trivial clauses:\n" ^
   112.1 --- a/src/HOL/Tools/semiring_normalizer.ML	Wed Nov 26 16:55:43 2014 +0100
   112.2 +++ b/src/HOL/Tools/semiring_normalizer.ML	Wed Nov 26 20:05:34 2014 +0100
   112.3 @@ -145,11 +145,11 @@
   112.4        val cz = rule 34 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg;
   112.5        val cn = rule 36 |> Thm.rhs_of |> Thm.dest_arg |> Thm.dest_arg;
   112.6        val ((clx, crx), (cly, cry)) =
   112.7 -        rule 13 |> Thm.rhs_of |> Thm.dest_binop |> pairself Thm.dest_binop;
   112.8 +        rule 13 |> Thm.rhs_of |> Thm.dest_binop |> apply2 Thm.dest_binop;
   112.9        val ((ca, cb), (cc, cd)) =
  112.10 -        rule 20 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_binop;
  112.11 +        rule 20 |> Thm.lhs_of |> Thm.dest_binop |> apply2 Thm.dest_binop;
  112.12        val cm = rule 1 |> Thm.rhs_of |> Thm.dest_arg;
  112.13 -      val (cp, cq) = rule 26 |> Thm.lhs_of |> Thm.dest_binop |> pairself Thm.dest_arg;
  112.14 +      val (cp, cq) = rule 26 |> Thm.lhs_of |> Thm.dest_binop |> apply2 Thm.dest_arg;
  112.15  
  112.16        val vars = [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry];
  112.17        val semiring = (sr_ops, sr_rules');
   113.1 --- a/src/HOL/Tools/set_comprehension_pointfree.ML	Wed Nov 26 16:55:43 2014 +0100
   113.2 +++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Wed Nov 26 20:05:34 2014 +0100
   113.3 @@ -78,7 +78,7 @@
   113.4  
   113.5  fun mk_prod1 Ts (t1, t2) =
   113.6    let
   113.7 -    val (T1, T2) = pairself (curry fastype_of1 Ts) (t1, t2)
   113.8 +    val (T1, T2) = apply2 (curry fastype_of1 Ts) (t1, t2)
   113.9    in
  113.10      HOLogic.pair_const T1 T2 $ t1 $ t2
  113.11    end;
  113.12 @@ -206,8 +206,8 @@
  113.13    end;
  113.14    
  113.15  fun map_atoms f (Atom a) = Atom (f a)
  113.16 -  | map_atoms f (Un (fm1, fm2)) = Un (pairself (map_atoms f) (fm1, fm2))
  113.17 -  | map_atoms f (Int (fm1, fm2)) = Int (pairself (map_atoms f) (fm1, fm2))
  113.18 +  | map_atoms f (Un (fm1, fm2)) = Un (apply2 (map_atoms f) (fm1, fm2))
  113.19 +  | map_atoms f (Int (fm1, fm2)) = Int (apply2 (map_atoms f) (fm1, fm2))
  113.20  
  113.21  fun extend Ts bs t = foldr1 mk_sigma (t :: map (fn b => HOLogic.mk_UNIV (nth Ts b)) bs)
  113.22  
  113.23 @@ -237,7 +237,7 @@
  113.24  fun merge_inter vs (pats1, fm1) (pats2, fm2) =
  113.25    let
  113.26      val pats = restricted_merge (map dest_Pattern pats1, map dest_Pattern pats2) 
  113.27 -    val (fm1', fm2') = pairself (adjust_atoms vs pats) (fm1, fm2)
  113.28 +    val (fm1', fm2') = apply2 (adjust_atoms vs pats) (fm1, fm2)
  113.29    in
  113.30      (map Pattern pats, Int (fm1', fm2'))
  113.31    end;
  113.32 @@ -245,7 +245,7 @@
  113.33  fun merge_union vs (pats1, fm1) (pats2, fm2) = 
  113.34    let
  113.35      val pats = merge (map dest_Pattern pats1, map dest_Pattern pats2)
  113.36 -    val (fm1', fm2') = pairself (adjust_atoms vs pats) (fm1, fm2)
  113.37 +    val (fm1', fm2') = apply2 (adjust_atoms vs pats) (fm1, fm2)
  113.38    in
  113.39      (map Pattern pats, Un (fm1', fm2'))
  113.40    end;
   114.1 --- a/src/HOL/Tools/try0.ML	Wed Nov 26 16:55:43 2014 +0100
   114.2 +++ b/src/HOL/Tools/try0.ML	Wed Nov 26 20:05:34 2014 +0100
   114.3 @@ -118,7 +118,7 @@
   114.4      val st = Proof.map_contexts (silence_methods false) st;
   114.5      fun trd (_, _, t) = t;
   114.6      fun par_map f =
   114.7 -      if mode = Normal then Par_List.map f #> map_filter I #> sort (int_ord o pairself trd)
   114.8 +      if mode = Normal then Par_List.map f #> map_filter I #> sort (int_ord o apply2 trd)
   114.9        else Par_List.get_some f #> the_list;
  114.10    in
  114.11      if mode = Normal then
   115.1 --- a/src/HOL/Word/WordBitwise.thy	Wed Nov 26 16:55:43 2014 +0100
   115.2 +++ b/src/HOL/Word/WordBitwise.thy	Wed Nov 26 20:05:34 2014 +0100
   115.3 @@ -510,7 +510,7 @@
   115.4    case term_of ct of
   115.5      (@{const upt} $ n $ m) =>
   115.6        let
   115.7 -        val (i, j) = pairself (snd o HOLogic.dest_number) (n, m);
   115.8 +        val (i, j) = apply2 (snd o HOLogic.dest_number) (n, m);
   115.9          val ns = map (Numeral.mk_cnumber @{ctyp nat}) (i upto (j - 1))
  115.10            |> mk_nat_clist;
  115.11          val prop = Thm.mk_binop @{cterm "op = :: nat list => _"} ct ns
   116.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Wed Nov 26 16:55:43 2014 +0100
   116.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Wed Nov 26 20:05:34 2014 +0100
   116.3 @@ -415,7 +415,7 @@
   116.4       let val c =
   116.5             fold (fn Lineq(_,_,l,_) => fn cs => union (op =) l cs) eqs []
   116.6             |> filter (fn i => i <> 0)
   116.7 -           |> sort (int_ord o pairself abs)
   116.8 +           |> sort (int_ord o apply2 abs)
   116.9             |> hd
  116.10           val (eq as Lineq(_,_,ceq,_),othereqs) =
  116.11                 extract_first (fn Lineq(_,_,l,_) => member (op =) l c) eqs
   117.1 --- a/src/Provers/hypsubst.ML	Wed Nov 26 16:55:43 2014 +0100
   117.2 +++ b/src/Provers/hypsubst.ML	Wed Nov 26 20:05:34 2014 +0100
   117.3 @@ -164,7 +164,7 @@
   117.4  
   117.5  fun inst_subst_tac ctxt b rl = CSUBGOAL (fn (cBi, i) =>
   117.6    case try (Logic.strip_assums_hyp #> hd #>
   117.7 -      Data.dest_Trueprop #> Data.dest_eq #> pairself contract) (Thm.term_of cBi) of
   117.8 +      Data.dest_Trueprop #> Data.dest_eq #> apply2 contract) (Thm.term_of cBi) of
   117.9      SOME (t, t') =>
  117.10        let
  117.11          val thy = Proof_Context.theory_of ctxt;
  117.12 @@ -183,10 +183,10 @@
  117.13              (case (if b then t else t') of
  117.14                Bound j => subst_bounds (map Bound ((1 upto j) @ 0 :: (j + 2 upto length ps)), Q)
  117.15              | t => Term.abstract_over (t, Term.incr_boundvars 1 Q));
  117.16 -        val (instT, _) = Thm.match (pairself (cterm_of thy o Logic.mk_type) (V, U));
  117.17 +        val (instT, _) = Thm.match (apply2 (cterm_of thy o Logic.mk_type) (V, U));
  117.18        in
  117.19          compose_tac ctxt (true, Drule.instantiate_normalize (instT,
  117.20 -          map (pairself (cterm_of thy))
  117.21 +          map (apply2 (cterm_of thy))
  117.22              [(Var (ixn, Ts ---> U --> body_type T), u),
  117.23               (Var (fst (dest_Var (head_of v1)), Ts ---> U), fold_rev Term.abs ps t),
  117.24               (Var (fst (dest_Var (head_of v2)), Ts ---> U), fold_rev Term.abs ps t')]) rl',
   118.1 --- a/src/Provers/splitter.ML	Wed Nov 26 16:55:43 2014 +0100
   118.2 +++ b/src/Provers/splitter.ML	Wed Nov 26 20:05:34 2014 +0100
   118.3 @@ -274,7 +274,7 @@
   118.4    in posns Ts [] [] t end;
   118.5  
   118.6  fun shorter ((_,ps,pos,_,_), (_,qs,qos,_,_)) =
   118.7 -  prod_ord (int_ord o pairself length) (order o pairself length)
   118.8 +  prod_ord (int_ord o apply2 length) (order o apply2 length)
   118.9      ((ps, pos), (qs, qos));
  118.10  
  118.11  
   119.1 --- a/src/Pure/Concurrent/par_exn.ML	Wed Nov 26 16:55:43 2014 +0100
   119.2 +++ b/src/Pure/Concurrent/par_exn.ML	Wed Nov 26 20:05:34 2014 +0100
   119.3 @@ -33,7 +33,7 @@
   119.4  fun the_serial exn =
   119.5    Markup.parse_int (the (Properties.get (Exn_Properties.get exn) Markup.serialN));
   119.6  
   119.7 -val exn_ord = rev_order o int_ord o pairself the_serial;
   119.8 +val exn_ord = rev_order o int_ord o apply2 the_serial;
   119.9  
  119.10  
  119.11  (* parallel exceptions *)
   120.1 --- a/src/Pure/General/file.ML	Wed Nov 26 16:55:43 2014 +0100
   120.2 +++ b/src/Pure/General/file.ML	Wed Nov 26 20:05:34 2014 +0100
   120.3 @@ -167,7 +167,7 @@
   120.4  (* eq *)
   120.5  
   120.6  fun eq paths =
   120.7 -  (case try (pairself (OS.FileSys.fileId o platform_path)) paths of
   120.8 +  (case try (apply2 (OS.FileSys.fileId o platform_path)) paths of
   120.9      SOME ids => is_equal (OS.FileSys.compare ids)
  120.10    | NONE => false);
  120.11  
   121.1 --- a/src/Pure/General/name_space.ML	Wed Nov 26 16:55:43 2014 +0100
   121.2 +++ b/src/Pure/General/name_space.ML	Wed Nov 26 20:05:34 2014 +0100
   121.3 @@ -152,7 +152,7 @@
   121.4      NONE => error (undefined kind name)
   121.5    | SOME (_, entry) => entry);
   121.6  
   121.7 -fun entry_ord space = int_ord o pairself (#serial o the_entry space);
   121.8 +fun entry_ord space = int_ord o apply2 (#serial o the_entry space);
   121.9  
  121.10  fun markup (Name_Space {kind, entries, ...}) name =
  121.11    (case Change_Table.lookup entries name of
  121.12 @@ -216,7 +216,7 @@
  121.13      else ext (get_accesses space name)
  121.14    end;
  121.15  
  121.16 -fun extern_ord ctxt space = string_ord o pairself (extern ctxt space);
  121.17 +fun extern_ord ctxt space = string_ord o apply2 (extern ctxt space);
  121.18  
  121.19  fun extern_shortest ctxt =
  121.20    extern
  121.21 @@ -235,9 +235,9 @@
  121.22    if Position.is_reported pos andalso xname <> "" andalso xname <> "_" then
  121.23      let
  121.24        fun result_ord ((xname1, (_, name1)), (xname2, (_, name2))) =
  121.25 -        (case bool_ord (pairself Long_Name.is_local (name2, name1)) of
  121.26 +        (case bool_ord (apply2 Long_Name.is_local (name2, name1)) of
  121.27            EQUAL =>
  121.28 -            (case int_ord (pairself Long_Name.qualification (xname1, xname2)) of
  121.29 +            (case int_ord (apply2 Long_Name.qualification (xname1, xname2)) of
  121.30                EQUAL => string_ord (xname1, xname2)
  121.31              | ord => ord)
  121.32          | ord => ord);
  121.33 @@ -373,7 +373,7 @@
  121.34      val spec = #2 (name_spec naming binding);
  121.35      val sfxs = mandatory_suffixes spec;
  121.36      val pfxs = mandatory_prefixes spec;
  121.37 -  in pairself (map Long_Name.implode) (sfxs @ pfxs, sfxs) end;
  121.38 +  in apply2 (map Long_Name.implode) (sfxs @ pfxs, sfxs) end;
  121.39  
  121.40  
  121.41  (* hide *)
   122.1 --- a/src/Pure/General/sha1_polyml.ML	Wed Nov 26 16:55:43 2014 +0100
   122.2 +++ b/src/Pure/General/sha1_polyml.ML	Wed Nov 26 20:05:34 2014 +0100
   122.3 @@ -15,7 +15,7 @@
   122.4  
   122.5  fun hex_string arr i =
   122.6    let val c = CInterface.fromCchar (CInterface.offset i CInterface.Cchar arr)
   122.7 -  in (op ^) (pairself hex_digit (Integer.div_mod (Char.ord c) 16)) end
   122.8 +  in (op ^) (apply2 hex_digit (Integer.div_mod (Char.ord c) 16)) end
   122.9  
  122.10  val lib_path =
  122.11    ("$ML_HOME/" ^ (if ML_System.platform_is_cygwin then "sha1.dll" else "libsha1.so"))
   123.1 --- a/src/Pure/Isar/calculation.ML	Wed Nov 26 16:55:43 2014 +0100
   123.2 +++ b/src/Pure/Isar/calculation.ML	Wed Nov 26 20:05:34 2014 +0100
   123.3 @@ -135,7 +135,7 @@
   123.4      val pretty_thm_item = Display.pretty_thm_item ctxt;
   123.5  
   123.6      val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of;
   123.7 -    val eq_prop = op aconv o pairself (Envir.beta_eta_contract o strip_assums_concl);
   123.8 +    val eq_prop = op aconv o apply2 (Envir.beta_eta_contract o strip_assums_concl);
   123.9      fun check_projection ths th =
  123.10        (case find_index (curry eq_prop th) ths of
  123.11          ~1 => Seq.Result [th]
   124.1 --- a/src/Pure/Isar/class.ML	Wed Nov 26 16:55:43 2014 +0100
   124.2 +++ b/src/Pure/Isar/class.ML	Wed Nov 26 20:05:34 2014 +0100
   124.3 @@ -215,7 +215,7 @@
   124.4      val operations = map (fn (v_ty as (_, ty), (c, _)) =>
   124.5        (c, (class, (ty, Free v_ty)))) params;
   124.6      val add_class = Graph.new_node (class,
   124.7 -        make_class_data (((map o pairself) fst params, base_sort,
   124.8 +        make_class_data (((map o apply2) fst params, base_sort,
   124.9            base_morph, export_morph, some_assm_intro, of_class, some_axiom), ([], operations)))
  124.10        #> fold (curry Graph.add_edge class) sups;
  124.11    in Class_Data.map add_class thy end;
   125.1 --- a/src/Pure/Isar/code.ML	Wed Nov 26 16:55:43 2014 +0100
   125.2 +++ b/src/Pure/Isar/code.ML	Wed Nov 26 20:05:34 2014 +0100
   125.3 @@ -655,7 +655,7 @@
   125.4      val ((abs, raw_ty), ((rep, rep_ty), param)) = (apsnd (apfst dest_Const o dest_comb)
   125.5          o apfst dest_Const o dest_comb) lhs
   125.6        handle TERM _ => bad_thm "Not an abstype certificate";
   125.7 -    val _ = pairself (fn c => if (is_some o Axclass.class_of_param thy) c
   125.8 +    val _ = apply2 (fn c => if (is_some o Axclass.class_of_param thy) c
   125.9        then error ("Is a class parameter: " ^ string_of_const thy c) else ()) (abs, rep);
  125.10      val _ = check_decl_ty thy (abs, raw_ty);
  125.11      val _ = check_decl_ty thy (rep, rep_ty);
  125.12 @@ -1035,12 +1035,12 @@
  125.13      val functions = the_functions exec
  125.14        |> Symtab.dest
  125.15        |> (map o apsnd) (snd o fst)
  125.16 -      |> sort (string_ord o pairself fst);
  125.17 +      |> sort (string_ord o apply2 fst);
  125.18      val datatypes = the_types exec
  125.19        |> Symtab.dest
  125.20        |> map (fn (tyco, (_, (vs, spec)) :: _) =>
  125.21            ((tyco, vs), constructors_of spec))
  125.22 -      |> sort (string_ord o pairself (fst o fst));
  125.23 +      |> sort (string_ord o apply2 (fst o fst));
  125.24      val cases = Symtab.dest ((fst o the_cases o the_exec) thy);
  125.25      val undefineds = Symtab.keys ((snd o the_cases o the_exec) thy);
  125.26    in
  125.27 @@ -1171,7 +1171,7 @@
  125.28      val T_cong = nth Ts pos;
  125.29      fun mk_prem z = Free (z, T_cong);
  125.30      fun mk_concl z = list_comb (Const (case_const, T), map2 (curry Free) (ws @ z :: vs) Ts);
  125.31 -    val (prem, concl) = pairself Logic.mk_equals (pairself mk_prem (x, y), pairself mk_concl (x, y));
  125.32 +    val (prem, concl) = apply2 Logic.mk_equals (apply2 mk_prem (x, y), apply2 mk_concl (x, y));
  125.33    in
  125.34      Goal.prove_sorry_global thy (x :: y :: zs) [prem] concl
  125.35        (fn {context = ctxt', prems} =>
   126.1 --- a/src/Pure/Isar/context_rules.ML	Wed Nov 26 16:55:43 2014 +0100
   126.2 +++ b/src/Pure/Isar/context_rules.ML	Wed Nov 26 20:05:34 2014 +0100
   126.3 @@ -119,7 +119,7 @@
   126.4        Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":")
   126.5          (map_filter (fn (_, (k, th)) =>
   126.6              if k = (i, b) then SOME (Display.pretty_thm_item ctxt th) else NONE)
   126.7 -          (sort (int_ord o pairself fst) rules));
   126.8 +          (sort (int_ord o apply2 fst) rules));
   126.9    in Pretty.writeln_chunks (map prt_kind rule_kinds) end;
  126.10  
  126.11  
  126.12 @@ -139,10 +139,10 @@
  126.13        else x :: untaglist rest;
  126.14  
  126.15  fun orderlist brls =
  126.16 -  untaglist (sort (prod_ord int_ord int_ord o pairself fst) brls);
  126.17 +  untaglist (sort (prod_ord int_ord int_ord o apply2 fst) brls);
  126.18  
  126.19  fun orderlist_no_weight brls =
  126.20 -  untaglist (sort (int_ord o pairself (snd o fst)) brls);
  126.21 +  untaglist (sort (int_ord o apply2 (snd o fst)) brls);
  126.22  
  126.23  fun may_unify weighted t net =
  126.24    map snd ((if weighted then orderlist else orderlist_no_weight) (Net.unify_term net t));
   127.1 --- a/src/Pure/Isar/generic_target.ML	Wed Nov 26 16:55:43 2014 +0100
   127.2 +++ b/src/Pure/Isar/generic_target.ML	Wed Nov 26 20:05:34 2014 +0100
   127.3 @@ -167,7 +167,7 @@
   127.4  
   127.5  fun background_abbrev (b, global_rhs) params =
   127.6    Local_Theory.background_theory_result (Sign.add_abbrev Print_Mode.internal (b, global_rhs))
   127.7 -  #>> pairself (fn t => Term.list_comb (Logic.unvarify_global t, params))
   127.8 +  #>> apply2 (fn t => Term.list_comb (Logic.unvarify_global t, params))
   127.9  
  127.10  
  127.11  (** lifting primitive to local theory operations **)
  127.12 @@ -190,7 +190,7 @@
  127.13      val mx' = check_mixfix lthy (b, extra_tfrees) mx;
  127.14  
  127.15      val type_params = map (Logic.mk_type o TFree) extra_tfrees;
  127.16 -    val term_params = map Free (sort (Variable.fixed_ord lthy o pairself #1) xs);
  127.17 +    val term_params = map Free (sort (Variable.fixed_ord lthy o apply2 #1) xs);
  127.18      val params = type_params @ term_params;
  127.19  
  127.20      val U = map Term.fastype_of params ---> T;
  127.21 @@ -247,8 +247,8 @@
  127.22  
  127.23      val instT = map_filter (fn (TVar v, T) => SOME (v, T) | _ => NONE) (tvars ~~ tfrees);
  127.24      val inst = filter (is_Var o fst) (vars ~~ frees);
  127.25 -    val cinstT = map (pairself certT o apfst TVar) instT;
  127.26 -    val cinst = map (pairself (cert o Term.map_types (Term_Subst.instantiateT instT))) inst;
  127.27 +    val cinstT = map (apply2 certT o apfst TVar) instT;
  127.28 +    val cinst = map (apply2 (cert o Term.map_types (Term_Subst.instantiateT instT))) inst;
  127.29      val result' = Thm.instantiate (cinstT, cinst) result;
  127.30  
  127.31      (*import assumes/defines*)
  127.32 @@ -287,7 +287,7 @@
  127.33      val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy);
  127.34  
  127.35      val rhs' = Assumption.export_term lthy (Local_Theory.target_of lthy) rhs;
  127.36 -    val term_params = map Free (sort (Variable.fixed_ord lthy o pairself #1) (Variable.add_fixed lthy rhs' []));
  127.37 +    val term_params = map Free (sort (Variable.fixed_ord lthy o apply2 #1) (Variable.add_fixed lthy rhs' []));
  127.38      val u = fold_rev lambda term_params rhs';
  127.39      val global_rhs = singleton (Variable.polymorphic thy_ctxt) u;
  127.40  
   128.1 --- a/src/Pure/Isar/local_defs.ML	Wed Nov 26 16:55:43 2014 +0100
   128.2 +++ b/src/Pure/Isar/local_defs.ML	Wed Nov 26 20:05:34 2014 +0100
   128.3 @@ -149,7 +149,7 @@
   128.4                      if t aconv u then (asm, false)
   128.5                      else (Drule.abs_def (Drule.gen_all asm), true))
   128.6                end)));
   128.7 -      in (pairself (map #1) (List.partition #2 defs_asms), th') end
   128.8 +      in (apply2 (map #1) (List.partition #2 defs_asms), th') end
   128.9    end;
  128.10  
  128.11  (*
   129.1 --- a/src/Pure/Isar/proof_context.ML	Wed Nov 26 16:55:43 2014 +0100
   129.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Nov 26 20:05:34 2014 +0100
   129.3 @@ -1176,7 +1176,7 @@
   129.4  
   129.5  fun dest_cases ctxt =
   129.6    Name_Space.fold_table (fn (a, (c, i)) => cons (i, (a, c))) (cases_of ctxt) []
   129.7 -  |> sort (int_ord o pairself #1) |> map #2;
   129.8 +  |> sort (int_ord o apply2 #1) |> map #2;
   129.9  
  129.10  local
  129.11  
  129.12 @@ -1255,7 +1255,7 @@
  129.13    let
  129.14      val space = const_space ctxt;
  129.15      val (constants, global_constants) =
  129.16 -      pairself (#constants o Consts.dest) (#consts (rep_data ctxt));
  129.17 +      apply2 (#constants o Consts.dest) (#consts (rep_data ctxt));
  129.18      val globals = Symtab.make global_constants;
  129.19      fun add_abbr (_, (_, NONE)) = I
  129.20        | add_abbr (c, (T, SOME t)) =
   130.1 --- a/src/Pure/Isar/rule_cases.ML	Wed Nov 26 16:55:43 2014 +0100
   130.2 +++ b/src/Pure/Isar/rule_cases.ML	Wed Nov 26 20:05:34 2014 +0100
   130.3 @@ -123,7 +123,7 @@
   130.4                (app (map (Term.dummy_pattern o #2) fixes2) (fold_rev Term.abs fixes2 t));
   130.5          val (assumes1, assumes2) =
   130.6            extract_assumes name hyp_names case_outline prop
   130.7 -          |> pairself (map (apsnd (maps Logic.dest_conjunctions)));
   130.8 +          |> apply2 (map (apsnd (maps Logic.dest_conjunctions)));
   130.9  
  130.10          val concl = Object_Logic.drop_judgment thy (Logic.strip_assums_concl prop);
  130.11          val binds =
  130.12 @@ -428,7 +428,7 @@
  130.13  local
  130.14  
  130.15  fun equal_cterms ts us =
  130.16 -  is_equal (list_ord (Term_Ord.fast_term_ord o pairself Thm.term_of) (ts, us));
  130.17 +  is_equal (list_ord (Term_Ord.fast_term_ord o apply2 Thm.term_of) (ts, us));
  130.18  
  130.19  fun prep_rule n th =
  130.20    let
   131.1 --- a/src/Pure/Isar/runtime.ML	Wed Nov 26 16:55:43 2014 +0100
   131.2 +++ b/src/Pure/Isar/runtime.ML	Wed Nov 26 20:05:34 2014 +0100
   131.3 @@ -119,7 +119,7 @@
   131.4              | _ => raised exn (robust (Pretty.string_of o Exn_Output.pretty) exn) []);
   131.5          in [((i, msg), id)] end)
   131.6        and sorted_msgs context exn =
   131.7 -        sort_distinct (int_ord o pairself (fst o fst)) (maps exn_msgs (flatten context exn));
   131.8 +        sort_distinct (int_ord o apply2 (fst o fst)) (maps exn_msgs (flatten context exn));
   131.9  
  131.10    in sorted_msgs NONE e end;
  131.11  
   132.1 --- a/src/Pure/ML/ml_context.ML	Wed Nov 26 16:55:43 2014 +0100
   132.2 +++ b/src/Pure/ML/ml_context.ML	Wed Nov 26 20:05:34 2014 +0100
   132.3 @@ -124,7 +124,7 @@
   132.4                    val keywords = Thy_Header.get_keywords' ctxt;
   132.5                    val (decl, ctxt') =
   132.6                      apply_antiquotation (Token.read_antiq keywords antiq (ss, #1 range)) ctxt;
   132.7 -                  val decl' = decl #> pairself (ML_Lex.tokenize #> map (ML_Lex.set_range range));
   132.8 +                  val decl' = decl #> apply2 (ML_Lex.tokenize #> map (ML_Lex.set_range range));
   132.9                  in (decl', ctxt') end;
  132.10  
  132.11            val ctxt =
  132.12 @@ -134,7 +134,7 @@
  132.13  
  132.14            val (decls, ctxt') = fold_map expand ants ctxt;
  132.15            val (ml_env, ml_body) =
  132.16 -            decls |> map (fn decl => decl ctxt') |> split_list |> pairself flat;
  132.17 +            decls |> map (fn decl => decl ctxt') |> split_list |> apply2 flat;
  132.18          in ((begin_env visible @ ml_env, ml_body), SOME (Context.Proof ctxt')) end;
  132.19    in ((ml_env @ end_env, ml_body), opt_ctxt') end;
  132.20  
   133.1 --- a/src/Pure/ML/ml_env.ML	Wed Nov 26 16:55:43 2014 +0100
   133.2 +++ b/src/Pure/ML/ml_env.ML	Wed Nov 26 20:05:34 2014 +0100
   133.3 @@ -57,8 +57,8 @@
   133.4    fun extend (data : T) = make_data (false, #tables data, #sml_tables data);
   133.5    fun merge (data : T * T) =
   133.6      make_data (false,
   133.7 -      merge_tables (pairself #tables data),
   133.8 -      merge_tables (pairself #sml_tables data));
   133.9 +      merge_tables (apply2 #tables data),
  133.10 +      merge_tables (apply2 #sml_tables data));
  133.11  );
  133.12  
  133.13  val inherit = Env.put o Env.get;
  133.14 @@ -85,7 +85,7 @@
  133.15          Context.thread_data ()
  133.16          |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#tables (Env.get context))))
  133.17          |> append (sel2 ML_Name_Space.global ()))
  133.18 -      |> sort_distinct (string_ord o pairself #1);
  133.19 +      |> sort_distinct (string_ord o apply2 #1);
  133.20  
  133.21      fun enter ap1 sel2 entry =
  133.22        if SML <> exchange then
   134.1 --- a/src/Pure/PIDE/command.ML	Wed Nov 26 16:55:43 2014 +0100
   134.2 +++ b/src/Pure/PIDE/command.ML	Wed Nov 26 20:05:34 2014 +0100
   134.3 @@ -187,7 +187,7 @@
   134.4  datatype eval = Eval of {exec_id: Document_ID.exec, eval_process: eval_state memo};
   134.5  
   134.6  fun eval_exec_id (Eval {exec_id, ...}) = exec_id;
   134.7 -val eval_eq = op = o pairself eval_exec_id;
   134.8 +val eval_eq = op = o apply2 eval_exec_id;
   134.9  
  134.10  val eval_running = Execution.is_running_exec o eval_exec_id;
  134.11  fun eval_finished (Eval {eval_process, ...}) = memo_finished eval_process;
  134.12 @@ -291,7 +291,7 @@
  134.13    exec_id: Document_ID.exec, print_process: unit memo};
  134.14  
  134.15  fun print_exec_id (Print {exec_id, ...}) = exec_id;
  134.16 -val print_eq = op = o pairself print_exec_id;
  134.17 +val print_eq = op = o apply2 print_exec_id;
  134.18  
  134.19  type print_fn = Toplevel.transition -> Toplevel.state -> unit;
  134.20  
   135.1 --- a/src/Pure/Proof/extraction.ML	Wed Nov 26 16:55:43 2014 +0100
   135.2 +++ b/src/Pure/Proof/extraction.ML	Wed Nov 26 20:05:34 2014 +0100
   135.3 @@ -103,14 +103,14 @@
   135.4            fun ren t = the_default t (Term.rename_abs tm1 tm t);
   135.5            val inc = Logic.incr_indexes ([], maxidx_of_term tm + 1);
   135.6            val env as (Tenv, tenv) = Pattern.match thy (inc tm1, tm) (Vartab.empty, Vartab.empty);
   135.7 -          val prems' = map (pairself (Envir.subst_term env o inc o ren)) prems;
   135.8 +          val prems' = map (apply2 (Envir.subst_term env o inc o ren)) prems;
   135.9            val env' = Envir.Envir
  135.10              {maxidx = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u) prems' ~1,
  135.11               tenv = tenv, tyenv = Tenv};
  135.12 -          val env'' = fold (Pattern.unify (Context.Theory thy) o pairself (lookup rew)) prems' env';
  135.13 +          val env'' = fold (Pattern.unify (Context.Theory thy) o apply2 (lookup rew)) prems' env';
  135.14          in SOME (Envir.norm_term env'' (inc (ren tm2)))
  135.15          end handle Pattern.MATCH => NONE | Pattern.Unif => NONE)
  135.16 -          (sort (int_ord o pairself fst)
  135.17 +          (sort (int_ord o apply2 fst)
  135.18              (Net.match_term rules (Envir.eta_contract tm)))
  135.19        end;
  135.20  
  135.21 @@ -207,7 +207,7 @@
  135.22      {realizes_eqns = merge_rules realizes_eqns1 realizes_eqns2,
  135.23       typeof_eqns = merge_rules typeof_eqns1 typeof_eqns2,
  135.24       types = AList.merge (op =) (K true) (types1, types2),
  135.25 -     realizers = Symtab.merge_list (eq_set (op =) o pairself #1) (realizers1, realizers2),
  135.26 +     realizers = Symtab.merge_list (eq_set (op =) o apply2 #1) (realizers1, realizers2),
  135.27       defs = Library.merge Thm.eq_thm (defs1, defs2),
  135.28       expand = Library.merge (op =) (expand1, expand2),
  135.29       prep = if is_some prep1 then prep1 else prep2};
   136.1 --- a/src/Pure/Proof/proof_checker.ML	Wed Nov 26 16:55:43 2014 +0100
   136.2 +++ b/src/Pure/Proof/proof_checker.ML	Wed Nov 26 20:05:34 2014 +0100
   136.3 @@ -78,7 +78,7 @@
   136.4            let
   136.5              val tvars = Term.add_tvars (Thm.full_prop_of thm) [] |> rev;
   136.6              val (fmap, thm') = Thm.varifyT_global' [] thm;
   136.7 -            val ctye = map (pairself (Thm.ctyp_of thy))
   136.8 +            val ctye = map (apply2 (Thm.ctyp_of thy))
   136.9                (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts)
  136.10            in
  136.11              Thm.instantiate (ctye, []) (forall_intr_vars (Thm.forall_intr_frees thm'))
   137.1 --- a/src/Pure/Proof/reconstruct.ML	Wed Nov 26 16:55:43 2014 +0100
   137.2 +++ b/src/Pure/Proof/reconstruct.ML	Wed Nov 26 20:05:34 2014 +0100
   137.3 @@ -100,7 +100,7 @@
   137.4        if a <> b then cantunify thy p
   137.5        else apfst flat (fold_map (decompose thy Ts) (ts ~~ us) (uT env T U))
   137.6    in
   137.7 -    case pairself (strip_comb o Envir.head_norm env) p of
   137.8 +    case apply2 (strip_comb o Envir.head_norm env) p of
   137.9        ((Const c, ts), (Const d, us)) => rigrig c d (unifyT thy) ts us
  137.10      | ((Free c, ts), (Free d, us)) => rigrig c d (unifyT thy) ts us
  137.11      | ((Bound i, ts), (Bound j, us)) =>
  137.12 @@ -254,7 +254,7 @@
  137.13        let
  137.14          fun search env [] = error ("Unsolvable constraints:\n" ^
  137.15                Pretty.string_of (Pretty.chunks (map (fn (_, p, _) =>
  137.16 -                Goal_Display.pretty_flexpair (Syntax.init_pretty_global thy) (pairself
  137.17 +                Goal_Display.pretty_flexpair (Syntax.init_pretty_global thy) (apply2
  137.18                    (Envir.norm_term bigenv) p)) cs)))
  137.19            | search env ((u, p as (t1, t2), vs)::ps) =
  137.20                if u then
  137.21 @@ -289,7 +289,7 @@
  137.22      val (t, prf, cs, env, _) = make_constraints_cprf thy
  137.23        (Envir.empty (Proofterm.maxidx_proof cprf ~1)) cprf';
  137.24      val cs' =
  137.25 -      map (pairself (Envir.norm_term env)) ((t, prop') :: cs)
  137.26 +      map (apply2 (Envir.norm_term env)) ((t, prop') :: cs)
  137.27        |> map (fn p => (true, p, Term.add_var_names (#1 p) (Term.add_var_names (#2 p) [])));
  137.28      val _ = message ("Solving remaining constraints (" ^ string_of_int (length cs') ^ ") ...");
  137.29      val env' = solve thy cs' env
   138.1 --- a/src/Pure/Syntax/syntax_phases.ML	Wed Nov 26 16:55:43 2014 +0100
   138.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Wed Nov 26 20:05:34 2014 +0100
   138.3 @@ -864,8 +864,8 @@
   138.4    let
   138.5      fun split_checks checks =
   138.6        List.partition (fn ((_, un), _) => not un) checks
   138.7 -      |> pairself (map (fn ((i, _), fs) => (i, map (fst o fst) fs))
   138.8 -          #> sort (int_ord o pairself fst));
   138.9 +      |> apply2 (map (fn ((i, _), fs) => (i, map (fst o fst) fs))
  138.10 +          #> sort (int_ord o apply2 fst));
  138.11      fun pretty_checks kind checks =
  138.12        checks |> map (fn (i, names) => Pretty.block
  138.13          [Pretty.str (kind ^ " (stage " ^ signed_string_of_int i ^ "):"),
  138.14 @@ -915,7 +915,7 @@
  138.15    let
  138.16      val funs = which (Checks.get (Context.Proof ctxt0))
  138.17        |> map_filter (fn ((i, u), fs) => if uncheck = u then SOME (i, map (snd o fst) fs) else NONE)
  138.18 -      |> Library.sort (int_ord o pairself fst) |> map snd
  138.19 +      |> Library.sort (int_ord o apply2 fst) |> map snd
  138.20        |> not uncheck ? map rev;
  138.21    in #1 (perhaps (check_all funs) (xs0, ctxt0)) end;
  138.22  
   139.1 --- a/src/Pure/System/message_channel.ML	Wed Nov 26 16:55:43 2014 +0100
   139.2 +++ b/src/Pure/System/message_channel.ML	Wed Nov 26 20:05:34 2014 +0100
   139.3 @@ -26,7 +26,7 @@
   139.4  
   139.5  fun message name raw_props body =
   139.6    let
   139.7 -    val robust_props = map (pairself YXML.embed_controls) raw_props;
   139.8 +    val robust_props = map (apply2 YXML.embed_controls) raw_props;
   139.9      val header = YXML.string_of (XML.Elem ((name, robust_props), []));
  139.10    in Message (chunk [header] @ chunk body) end;
  139.11  
   140.1 --- a/src/Pure/Thy/present.ML	Wed Nov 26 16:55:43 2014 +0100
   140.2 +++ b/src/Pure/Thy/present.ML	Wed Nov 26 20:05:34 2014 +0100
   140.3 @@ -277,7 +277,7 @@
   140.4  
   140.5  (* finish session -- output all generated text *)
   140.6  
   140.7 -fun sorted_index index = map snd (sort (int_ord o pairself fst) (rev index));
   140.8 +fun sorted_index index = map snd (sort (int_ord o apply2 fst) (rev index));
   140.9  fun index_buffer index = Buffer.add (implode (sorted_index index)) Buffer.empty;
  140.10  
  140.11  fun write_tex src name path =
   141.1 --- a/src/Pure/Tools/build.ML	Wed Nov 26 16:55:43 2014 +0100
   141.2 +++ b/src/Pure/Tools/build.ML	Wed Nov 26 20:05:34 2014 +0100
   141.3 @@ -147,7 +147,7 @@
   141.4            (Options.bool options "document_graph")
   141.5            (Options.string options "document_output")
   141.6            (Present.document_variants (Options.string options "document_variants"))
   141.7 -          (map (pairself Path.explode) document_files)
   141.8 +          (map (apply2 Path.explode) document_files)
   141.9            parent_name (chapter, name)
  141.10            verbose;
  141.11  
   142.1 --- a/src/Pure/Tools/class_deps.ML	Wed Nov 26 16:55:43 2014 +0100
   142.2 +++ b/src/Pure/Tools/class_deps.ML	Wed Nov 26 20:05:34 2014 +0100
   142.3 @@ -30,7 +30,7 @@
   142.4              dir = "", unfold = true, path = "", content = []});
   142.5      val gr =
   142.6        Graph.fold (cons o entry) classes []
   142.7 -      |> sort (int_ord o pairself #1) |> map #2;
   142.8 +      |> sort (int_ord o apply2 #1) |> map #2;
   142.9    in Graph_Display.display_graph gr end;
  142.10  
  142.11  val visualize = gen_visualize (Type.cert_sort o Proof_Context.tsig_of);
   143.1 --- a/src/Pure/Tools/find_consts.ML	Wed Nov 26 16:55:43 2014 +0100
   143.2 +++ b/src/Pure/Tools/find_consts.ML	Wed Nov 26 20:05:34 2014 +0100
   143.3 @@ -110,7 +110,7 @@
   143.4  
   143.5      val matches =
   143.6        fold (fn c => (case eval_entry c of NONE => I | SOME rank => cons (rank, c))) constants []
   143.7 -      |> sort (prod_ord (rev_order o int_ord) (string_ord o pairself fst))
   143.8 +      |> sort (prod_ord (rev_order o int_ord) (string_ord o apply2 fst))
   143.9        |> map (apsnd fst o snd);
  143.10  
  143.11      val position_markup = Position.markup (Position.thread_data ()) Markup.position;
   144.1 --- a/src/Pure/Tools/find_theorems.ML	Wed Nov 26 16:55:43 2014 +0100
   144.2 +++ b/src/Pure/Tools/find_theorems.ML	Wed Nov 26 20:05:34 2014 +0100
   144.3 @@ -330,9 +330,9 @@
   144.4  local
   144.5  
   144.6  val index_ord = option_ord (K EQUAL);
   144.7 -val hidden_ord = bool_ord o pairself Long_Name.is_hidden;
   144.8 -val qual_ord = int_ord o pairself Long_Name.qualification;
   144.9 -val txt_ord = int_ord o pairself size;
  144.10 +val hidden_ord = bool_ord o apply2 Long_Name.is_hidden;
  144.11 +val qual_ord = int_ord o apply2 Long_Name.qualification;
  144.12 +val txt_ord = int_ord o apply2 size;
  144.13  
  144.14  fun nicer_name (x, i) (y, j) =
  144.15    (case hidden_ord (x, y) of EQUAL =>
  144.16 @@ -368,9 +368,9 @@
  144.17  
  144.18  fun rem_thm_dups nicer xs =
  144.19    (xs ~~ (1 upto length xs))
  144.20 -  |> sort (Term_Ord.fast_term_ord o pairself (Thm.full_prop_of o #2 o #1))
  144.21 +  |> sort (Term_Ord.fast_term_ord o apply2 (Thm.full_prop_of o #2 o #1))
  144.22    |> rem_cdups nicer
  144.23 -  |> sort (int_ord o pairself #2)
  144.24 +  |> sort (int_ord o apply2 #2)
  144.25    |> map #1;
  144.26  
  144.27  end;
   145.1 --- a/src/Pure/Tools/plugin.ML	Wed Nov 26 16:55:43 2014 +0100
   145.2 +++ b/src/Pure/Tools/plugin.ML	Wed Nov 26 20:05:34 2014 +0100
   145.3 @@ -112,8 +112,8 @@
   145.4  type data = {filter: Plugin_Name.filter, naming: Name_Space.naming, value: T, id: serial};
   145.5  type interp = {name: string, apply: T -> local_theory -> local_theory, id: serial};
   145.6  
   145.7 -val eq_data: data * data -> bool = op = o pairself #id;
   145.8 -val eq_interp: interp * interp -> bool = op = o pairself #id;
   145.9 +val eq_data: data * data -> bool = op = o apply2 #id;
  145.10 +val eq_interp: interp * interp -> bool = op = o apply2 #id;
  145.11  
  145.12  fun mk_data filter naming x : data = {filter = filter, naming = naming, value = x, id = serial ()};
  145.13  fun mk_interp name f : interp = {name = name, apply = f, id = serial ()};
   146.1 --- a/src/Pure/Tools/rail.ML	Wed Nov 26 16:55:43 2014 +0100
   146.2 +++ b/src/Pure/Tools/rail.ML	Wed Nov 26 20:05:34 2014 +0100
   146.3 @@ -265,11 +265,11 @@
   146.4  fun prepare_trees (CAT (ts, _)) = Cat (0, map prepare_tree ts)
   146.5  and prepare_tree (BAR (Ts, _)) = bar (map prepare_trees Ts)
   146.6    | prepare_tree (STAR (Ts, _)) =
   146.7 -      let val (cat1, cat2) = pairself prepare_trees Ts in
   146.8 +      let val (cat1, cat2) = apply2 prepare_trees Ts in
   146.9          if is_empty cat2 then plus (empty, cat1)
  146.10          else bar [empty, cat [plus (cat1, cat2)]]
  146.11        end
  146.12 -  | prepare_tree (PLUS (Ts, _)) = plus (pairself prepare_trees Ts)
  146.13 +  | prepare_tree (PLUS (Ts, _)) = plus (apply2 prepare_trees Ts)
  146.14    | prepare_tree (MAYBE (t, _)) = bar [empty, cat [prepare_tree t]]
  146.15    | prepare_tree (NEWLINE _) = Newline 0
  146.16    | prepare_tree (NONTERMINAL (a, _)) = Nonterminal a
   147.1 --- a/src/Pure/Tools/rule_insts.ML	Wed Nov 26 16:55:43 2014 +0100
   147.2 +++ b/src/Pure/Tools/rule_insts.ML	Wed Nov 26 20:05:34 2014 +0100
   147.3 @@ -118,7 +118,7 @@
   147.4      val inst_tvars = map_filter (make_instT (instT2 o instT1)) tvars;
   147.5      val inst_vars = map_filter (make_inst inst2) vars2;
   147.6    in
   147.7 -    (map (pairself certT) inst_tvars, map (pairself cert) inst_vars)
   147.8 +    (map (apply2 certT) inst_tvars, map (apply2 cert) inst_vars)
   147.9    end;
  147.10  
  147.11  fun where_rule ctxt mixed_insts fixes thm =
  147.12 @@ -251,7 +251,7 @@
  147.13          val cenv =
  147.14            map
  147.15              (fn (xi, t) =>
  147.16 -              pairself (Thm.cterm_of thy) (Var (xi, fastype_of t), t))
  147.17 +              apply2 (Thm.cterm_of thy) (Var (xi, fastype_of t), t))
  147.18              (distinct
  147.19                (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2)
  147.20                (xis ~~ ts));
  147.21 @@ -265,7 +265,7 @@
  147.22          fun liftterm t =
  147.23            fold_rev absfree (param_names ~~ paramTs) (Logic.incr_indexes (paramTs, inc) t);
  147.24          fun liftpair (cv, ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct);
  147.25 -        val lifttvar = pairself (ctyp_of thy o Logic.incr_tvar inc);
  147.26 +        val lifttvar = apply2 (ctyp_of thy o Logic.incr_tvar inc);
  147.27          val rule = Drule.instantiate_normalize
  147.28                (map lifttvar envT', map liftpair cenv)
  147.29                (Thm.lift_rule cgoal thm)
   148.1 --- a/src/Pure/Tools/thm_deps.ML	Wed Nov 26 16:55:43 2014 +0100
   148.2 +++ b/src/Pure/Tools/thm_deps.ML	Wed Nov 26 20:05:34 2014 +0100
   148.3 @@ -68,7 +68,7 @@
   148.4  
   148.5      val new_thms =
   148.6        fold (add_facts o Global_Theory.facts_of) thys []
   148.7 -      |> sort_distinct (string_ord o pairself #1);
   148.8 +      |> sort_distinct (string_ord o apply2 #1);
   148.9  
  148.10      val used =
  148.11        Proofterm.fold_body_thms
   149.1 --- a/src/Pure/axclass.ML	Wed Nov 26 16:55:43 2014 +0100
   149.2 +++ b/src/Pure/axclass.ML	Wed Nov 26 20:05:34 2014 +0100
   149.3 @@ -321,7 +321,7 @@
   149.4  fun cert_classrel thy raw_rel =
   149.5    let
   149.6      val string_of_sort = Syntax.string_of_sort_global thy;
   149.7 -    val (c1, c2) = pairself (Sign.certify_class thy) raw_rel;
   149.8 +    val (c1, c2) = apply2 (Sign.certify_class thy) raw_rel;
   149.9      val _ = Sign.primitive_classrel (c1, c2) thy;
  149.10      val _ =
  149.11        (case subtract (op =) (all_params_of thy [c1]) (all_params_of thy [c2]) of
  149.12 @@ -331,7 +331,7 @@
  149.13    in (c1, c2) end;
  149.14  
  149.15  fun read_classrel thy raw_rel =
  149.16 -  cert_classrel thy (pairself (Proof_Context.read_class (Proof_Context.init_global thy)) raw_rel)
  149.17 +  cert_classrel thy (apply2 (Proof_Context.read_class (Proof_Context.init_global thy)) raw_rel)
  149.18      handle TYPE (msg, _, _) => error msg;
  149.19  
  149.20  
   150.1 --- a/src/Pure/context.ML	Wed Nov 26 16:55:43 2014 +0100
   150.2 +++ b/src/Pure/context.ML	Wed Nov 26 20:05:34 2014 +0100
   150.3 @@ -145,7 +145,7 @@
   150.4    in k end;
   150.5  
   150.6  val extend_data = Datatab.map invoke_extend;
   150.7 -fun merge_data pp = Datatab.join (invoke_merge pp) o pairself extend_data;
   150.8 +fun merge_data pp = Datatab.join (invoke_merge pp) o apply2 extend_data;
   150.9  
  150.10  end;
  150.11  
  150.12 @@ -238,7 +238,7 @@
  150.13  
  150.14  (* equality and inclusion *)
  150.15  
  150.16 -val eq_thy = op = o pairself (#id o identity_of);
  150.17 +val eq_thy = op = o apply2 (#id o identity_of);
  150.18  
  150.19  fun proper_subthy (Theory ({id, ...}, _, _, _), Theory ({ids, ...}, _, _, _)) =
  150.20    Inttab.defined ids id;
   151.1 --- a/src/Pure/drule.ML	Wed Nov 26 16:55:43 2014 +0100
   151.2 +++ b/src/Pure/drule.ML	Wed Nov 26 20:05:34 2014 +0100
   151.3 @@ -797,7 +797,7 @@
   151.4          val instT =
   151.5            Vartab.fold (fn (xi, (S, T)) =>
   151.6              cons (certT (TVar (xi, S)), certT (Envir.norm_type tye T))) tye [];
   151.7 -        val inst = map (pairself (Thm.instantiate_cterm (instT, []))) ctpairs;
   151.8 +        val inst = map (apply2 (Thm.instantiate_cterm (instT, []))) ctpairs;
   151.9        in instantiate_normalize (instT, inst) th end
  151.10        handle TERM (msg, _) => raise THM (msg, 0, [th])
  151.11          | TYPE (msg, _, _) => raise THM (msg, 0, [th]);
   152.1 --- a/src/Pure/facts.ML	Wed Nov 26 16:55:43 2014 +0100
   152.2 +++ b/src/Pure/facts.ML	Wed Nov 26 20:05:34 2014 +0100
   152.3 @@ -206,7 +206,7 @@
   152.4  
   152.5  (* indexed props *)
   152.6  
   152.7 -val prop_ord = Term_Ord.term_ord o pairself Thm.full_prop_of;
   152.8 +val prop_ord = Term_Ord.term_ord o apply2 Thm.full_prop_of;
   152.9  
  152.10  fun props (Facts {props, ...}) = sort_distinct prop_ord (Net.content props);
  152.11  fun could_unify (Facts {props, ...}) = Net.unify_term props;
   153.1 --- a/src/Pure/item_net.ML	Wed Nov 26 16:55:43 2014 +0100
   153.2 +++ b/src/Pure/item_net.ML	Wed Nov 26 20:05:34 2014 +0100
   153.3 @@ -64,7 +64,7 @@
   153.4  fun remove x (items as Items {eq, index, content, next, net}) =
   153.5    if member items x then
   153.6      mk_items eq index (Library.remove eq x content) next
   153.7 -      (fold (fn t => Net.delete_term_safe (eq o pairself #2) (t, (0, x))) (index x) net)
   153.8 +      (fold (fn t => Net.delete_term_safe (eq o apply2 #2) (t, (0, x))) (index x) net)
   153.9    else items;
  153.10  
  153.11  fun update x items = cons x (remove x items);
   154.1 --- a/src/Pure/library.ML	Wed Nov 26 16:55:43 2014 +0100
   154.2 +++ b/src/Pure/library.ML	Wed Nov 26 20:05:34 2014 +0100
   154.3 @@ -44,7 +44,7 @@
   154.4    val swap: 'a * 'b -> 'b * 'a
   154.5    val apfst: ('a -> 'b) -> 'a * 'c -> 'b * 'c
   154.6    val apsnd: ('a -> 'b) -> 'c * 'a -> 'c * 'b
   154.7 -  val pairself: ('a -> 'b) -> 'a * 'a -> 'b * 'b
   154.8 +  val apply2: ('a -> 'b) -> 'a * 'a -> 'b * 'b
   154.9  
  154.10    (*booleans*)
  154.11    val equal: ''a -> ''a -> bool
  154.12 @@ -283,7 +283,7 @@
  154.13  
  154.14  fun apfst f (x, y) = (f x, y);
  154.15  fun apsnd f (x, y) = (x, f y);
  154.16 -fun pairself f (x, y) = (f x, f y);
  154.17 +fun apply2 f (x, y) = (f x, f y);
  154.18  
  154.19  
  154.20  (* booleans *)
  154.21 @@ -964,7 +964,7 @@
  154.22  fun sort_distinct ord = mergesort true ord;
  154.23  
  154.24  val sort_strings = sort string_ord;
  154.25 -fun sort_wrt key xs = sort (string_ord o pairself key) xs;
  154.26 +fun sort_wrt key xs = sort (string_ord o apply2 key) xs;
  154.27  
  154.28  
  154.29  (* items tagged by integer index *)
  154.30 @@ -981,7 +981,7 @@
  154.31        else x :: untag_list rest;
  154.32  
  154.33  (*return list elements in original order*)
  154.34 -fun order_list list = untag_list (sort (int_ord o pairself fst) list);
  154.35 +fun order_list list = untag_list (sort (int_ord o apply2 fst) list);
  154.36  
  154.37  
  154.38  
   155.1 --- a/src/Pure/more_thm.ML	Wed Nov 26 16:55:43 2014 +0100
   155.2 +++ b/src/Pure/more_thm.ML	Wed Nov 26 20:05:34 2014 +0100
   155.3 @@ -112,7 +112,7 @@
   155.4  
   155.5  (* collecting cterms *)
   155.6  
   155.7 -val op aconvc = op aconv o pairself Thm.term_of;
   155.8 +val op aconvc = op aconv o apply2 Thm.term_of;
   155.9  
  155.10  fun add_cterm_frees ct =
  155.11    let
  155.12 @@ -179,7 +179,7 @@
  155.13  
  155.14  (* tables and caches *)
  155.15  
  155.16 -structure Ctermtab = Table(type key = cterm val ord = Term_Ord.fast_term_ord o pairself Thm.term_of);
  155.17 +structure Ctermtab = Table(type key = cterm val ord = Term_Ord.fast_term_ord o apply2 Thm.term_of);
  155.18  structure Thmtab = Table(type key = thm val ord = thm_ord);
  155.19  
  155.20  fun cterm_cache f = Cache.create Ctermtab.empty Ctermtab.lookup Ctermtab.update f;
  155.21 @@ -193,11 +193,11 @@
  155.22  
  155.23  val eq_thm = is_equal o thm_ord;
  155.24  
  155.25 -val eq_thm_prop = op aconv o pairself Thm.full_prop_of;
  155.26 +val eq_thm_prop = op aconv o apply2 Thm.full_prop_of;
  155.27  
  155.28  fun eq_thm_strict ths =
  155.29    eq_thm ths andalso
  155.30 -    let val (rep1, rep2) = pairself Thm.rep_thm ths in
  155.31 +    let val (rep1, rep2) = apply2 Thm.rep_thm ths in
  155.32        Theory.eq_thy (#thy rep1, #thy rep2) andalso
  155.33        #maxidx rep1 = #maxidx rep2 andalso
  155.34        #tags rep1 = #tags rep2
  155.35 @@ -207,7 +207,7 @@
  155.36  (* pattern equivalence *)
  155.37  
  155.38  fun equiv_thm ths =
  155.39 -  Pattern.equiv (Theory.merge (pairself Thm.theory_of_thm ths)) (pairself Thm.full_prop_of ths);
  155.40 +  Pattern.equiv (Theory.merge (apply2 Thm.theory_of_thm ths)) (apply2 Thm.full_prop_of ths);
  155.41  
  155.42  
  155.43  (* type classes and sorts *)
  155.44 @@ -397,7 +397,7 @@
  155.45      val tfrees = rev (map TFree (Term.add_tfrees t []));
  155.46      val tfrees' = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT (length tfrees));
  155.47      val strip = tfrees ~~ tfrees';
  155.48 -    val recover = map (pairself (Thm.ctyp_of thy o Logic.varifyT_global) o swap) strip;
  155.49 +    val recover = map (apply2 (Thm.ctyp_of thy o Logic.varifyT_global) o swap) strip;
  155.50      val t' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip))) t;
  155.51    in (strip, recover, t') end;
  155.52  
   156.1 --- a/src/Pure/proofterm.ML	Wed Nov 26 16:55:43 2014 +0100
   156.2 +++ b/src/Pure/proofterm.ML	Wed Nov 26 20:05:34 2014 +0100
   156.3 @@ -1226,7 +1226,7 @@
   156.4        | (f $ t, g $ u) => mtch (mtch instsp (f, g)) (t, u)
   156.5        | (Bound i, Bound j) => if i=j then instsp else raise PMatch
   156.6        | _ => raise PMatch
   156.7 -  in mtch instsp (pairself Envir.beta_eta_contract p) end;
   156.8 +  in mtch instsp (apply2 Envir.beta_eta_contract p) end;
   156.9  
  156.10  fun match_proof Ts tymatch =
  156.11    let
   157.1 --- a/src/Pure/raw_simplifier.ML	Wed Nov 26 16:55:43 2014 +0100
   157.2 +++ b/src/Pure/raw_simplifier.ML	Wed Nov 26 20:05:34 2014 +0100
   157.3 @@ -342,7 +342,7 @@
   157.4        val rules' = Net.merge eq_rrule (rules1, rules2);
   157.5        val prems' = Thm.merge_thms (prems1, prems2);
   157.6        val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1;
   157.7 -      val congs' = merge (Thm.eq_thm_prop o pairself #2) (congs1, congs2);
   157.8 +      val congs' = merge (Thm.eq_thm_prop o apply2 #2) (congs1, congs2);
   157.9        val weak' = merge (op =) (weak1, weak2);
  157.10        val procs' = Net.merge eq_proc (procs1, procs2);
  157.11        val loop_tacs' = AList.merge (op =) (K true) (loop_tacs1, loop_tacs2);
  157.12 @@ -1036,7 +1036,7 @@
  157.13          (case check_conv ctxt true (Drule.beta_eta_conversion t) thm2 of
  157.14            NONE => err ("Congruence proof failed.  Should not have proved", thm2)
  157.15          | SOME thm2' =>
  157.16 -            if op aconv (pairself term_of (Thm.dest_equals (cprop_of thm2')))
  157.17 +            if op aconv (apply2 term_of (Thm.dest_equals (cprop_of thm2')))
  157.18              then NONE else SOME thm2'))
  157.19    end;
  157.20  
   158.1 --- a/src/Pure/search.ML	Wed Nov 26 16:55:43 2014 +0100
   158.2 +++ b/src/Pure/search.ML	Wed Nov 26 20:05:34 2014 +0100
   158.3 @@ -194,7 +194,7 @@
   158.4  structure Thm_Heap = Heap
   158.5  (
   158.6    type elem = int * thm;
   158.7 -  val ord = prod_ord int_ord (Term_Ord.term_ord o pairself Thm.prop_of);
   158.8 +  val ord = prod_ord int_ord (Term_Ord.term_ord o apply2 Thm.prop_of);
   158.9  );
  158.10  
  158.11  val trace_BEST_FIRST = Unsynchronized.ref false;
   159.1 --- a/src/Pure/subgoal.ML	Wed Nov 26 16:55:43 2014 +0100
   159.2 +++ b/src/Pure/subgoal.ML	Wed Nov 26 20:05:34 2014 +0100
   159.3 @@ -86,7 +86,7 @@
   159.4            else (Ts ---> T, ts);
   159.5          val u = Free (y, U);
   159.6          in ((Var v, list_comb (u, args)), (u, Var ((x, i + idx), U))) end;
   159.7 -    val (inst1, inst2) = split_list (map (pairself (pairself cert)) (map2 var_inst vars ys));
   159.8 +    val (inst1, inst2) = split_list (map (apply2 (apply2 cert)) (map2 var_inst vars ys));
   159.9  
  159.10      val th'' = Thm.instantiate ([], inst1) th';
  159.11    in ((inst2, th''), ctxt'') end;
   160.1 --- a/src/Pure/thm.ML	Wed Nov 26 16:55:43 2014 +0100
   160.2 +++ b/src/Pure/thm.ML	Wed Nov 26 20:05:34 2014 +0100
   160.3 @@ -338,7 +338,7 @@
   160.4    let fun cterm max t = Cterm {thy = thy, t = t, T = propT, maxidx = max, sorts = shyps} in
   160.5     {thy = thy, tags = tags, maxidx = maxidx, shyps = shyps,
   160.6      hyps = map (cterm ~1) hyps,
   160.7 -    tpairs = map (pairself (cterm maxidx)) tpairs,
   160.8 +    tpairs = map (apply2 (cterm maxidx)) tpairs,
   160.9      prop = cterm maxidx prop}
  160.10    end;
  160.11  
  160.12 @@ -1000,7 +1000,7 @@
  160.13        if Envir.is_empty env then th
  160.14        else
  160.15          let
  160.16 -          val tpairs' = tpairs |> map (pairself (Envir.norm_term env))
  160.17 +          val tpairs' = tpairs |> map (apply2 (Envir.norm_term env))
  160.18              (*remove trivial tpairs, of the form t==t*)
  160.19              |> filter_out (op aconv);
  160.20            val der' = deriv_rule1 (Proofterm.norm_proof' env) der;
  160.21 @@ -1039,7 +1039,7 @@
  160.22  
  160.23          val gen = Term_Subst.generalize (tfrees, frees) idx;
  160.24          val prop' = gen prop;
  160.25 -        val tpairs' = map (pairself gen) tpairs;
  160.26 +        val tpairs' = map (apply2 gen) tpairs;
  160.27          val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop');
  160.28        in
  160.29          Thm (deriv_rule1 (Proofterm.generalize (tfrees, frees) idx) der,
  160.30 @@ -1291,7 +1291,7 @@
  160.31          maxidx = maxidx + inc,
  160.32          shyps = Sorts.union shyps sorts,  (*sic!*)
  160.33          hyps = hyps,
  160.34 -        tpairs = map (pairself lift_abs) tpairs,
  160.35 +        tpairs = map (apply2 lift_abs) tpairs,
  160.36          prop = Logic.list_implies (map lift_all As, lift_all B)})
  160.37    end;
  160.38  
  160.39 @@ -1305,7 +1305,7 @@
  160.40        maxidx = maxidx + i,
  160.41        shyps = shyps,
  160.42        hyps = hyps,
  160.43 -      tpairs = map (pairself (Logic.incr_indexes ([], i))) tpairs,
  160.44 +      tpairs = map (apply2 (Logic.incr_indexes ([], i))) tpairs,
  160.45        prop = Logic.incr_indexes ([], i) prop});
  160.46  
  160.47  (*Solve subgoal Bi of proof state B1...Bn/C by assumption. *)
  160.48 @@ -1324,7 +1324,7 @@
  160.49          hyps = hyps,
  160.50          tpairs =
  160.51            if Envir.is_empty env then tpairs
  160.52 -          else map (pairself (Envir.norm_term env)) tpairs,
  160.53 +          else map (apply2 (Envir.norm_term env)) tpairs,
  160.54          prop =
  160.55            if Envir.is_empty env then (*avoid wasted normalizations*)
  160.56              Logic.list_implies (Bs, C)
  160.57 @@ -1504,7 +1504,7 @@
  160.58            |> fold (add_var o snd) tpairs;
  160.59          val vids' = fold (add_var o strip_lifted B) As [];
  160.60          (*unknowns appearing elsewhere be preserved!*)
  160.61 -        val al' = distinct ((op =) o pairself fst)
  160.62 +        val al' = distinct ((op =) o apply2 fst)
  160.63            (filter_out (fn (x, y) =>
  160.64               not (member (op =) vids' x) orelse
  160.65               member (op =) vids x orelse member (op =) vids y) al);
  160.66 @@ -1598,7 +1598,7 @@
  160.67             val (ntpairs, normp) =
  160.68               if Envir.is_empty env then (tpairs, (Bs @ As, C))
  160.69               else
  160.70 -             let val ntps = map (pairself normt) tpairs
  160.71 +             let val ntps = map (apply2 normt) tpairs
  160.72               in if Envir.above env smax then
  160.73                    (*no assignments in state; normalize the rule only*)
  160.74                    if lifted
   161.1 --- a/src/Pure/type.ML	Wed Nov 26 16:55:43 2014 +0100
   161.2 +++ b/src/Pure/type.ML	Wed Nov 26 20:05:34 2014 +0100
   161.3 @@ -188,7 +188,7 @@
   161.4    let
   161.5      val log_types =
   161.6        Name_Space.fold_table (fn (c, LogicalType n) => cons (c, n) | _ => I) types []
   161.7 -      |> Library.sort (int_ord o pairself snd) |> map fst;
   161.8 +      |> Library.sort (int_ord o apply2 snd) |> map fst;
   161.9    in make_tsig (classes, default, types, log_types) end;
  161.10  
  161.11  fun map_tsig f (TSig {classes, default, types, log_types = _}) =
  161.12 @@ -639,7 +639,7 @@
  161.13  fun add_classrel pp rel tsig =
  161.14    tsig |> map_tsig (fn ((space, classes), default, types) =>
  161.15      let
  161.16 -      val rel' = pairself (cert_class tsig) rel
  161.17 +      val rel' = apply2 (cert_class tsig) rel
  161.18          handle TYPE (msg, _, _) => error msg;
  161.19        val classes' = classes |> Sorts.add_classrel pp rel';
  161.20      in ((space, classes'), default, types) end);
   162.1 --- a/src/Pure/type_infer_context.ML	Wed Nov 26 16:55:43 2014 +0100
   162.2 +++ b/src/Pure/type_infer_context.ML	Wed Nov 26 20:05:34 2014 +0100
   162.3 @@ -219,7 +219,7 @@
   162.4        quote (Syntax.string_of_typ ctxt (Type (a, replicate (length Ts) dummyT)));
   162.5  
   162.6      fun unif (T1, T2) (env as (tye, _)) =
   162.7 -      (case pairself (`Type_Infer.is_paramT o Type_Infer.deref tye) (T1, T2) of
   162.8 +      (case apply2 (`Type_Infer.is_paramT o Type_Infer.deref tye) (T1, T2) of
   162.9          ((true, TVar (xi, S)), (_, T)) => assign xi T S env
  162.10        | ((_, T), (true, TVar (xi, S))) => assign xi T S env
  162.11        | ((_, Type (a, Ts)), (_, Type (b, Us))) =>
   163.1 --- a/src/Pure/variable.ML	Wed Nov 26 16:55:43 2014 +0100
   163.2 +++ b/src/Pure/variable.ML	Wed Nov 26 20:05:34 2014 +0100
   163.3 @@ -352,7 +352,7 @@
   163.4  
   163.5  fun dest_fixes ctxt =
   163.6    Name_Space.fold_table (fn (x, y) => cons (y, x)) (fixes_of ctxt) []
   163.7 -  |> sort (Name_Space.entry_ord (fixes_space ctxt) o pairself #2);
   163.8 +  |> sort (Name_Space.entry_ord (fixes_space ctxt) o apply2 #2);
   163.9  
  163.10  
  163.11  (* collect variables *)
  163.12 @@ -403,7 +403,7 @@
  163.13          [] => ()
  163.14        | bads => error ("Illegal internal Skolem constant(s): " ^ commas (map Binding.print bads)));
  163.15      val _ =
  163.16 -      (case duplicates (op = o pairself Binding.name_of) bs of
  163.17 +      (case duplicates (op = o apply2 Binding.name_of) bs of
  163.18          [] => ()
  163.19        | dups => err_dups dups);
  163.20  
   164.1 --- a/src/Tools/Code/code_namespace.ML	Wed Nov 26 16:55:43 2014 +0100
   164.2 +++ b/src/Tools/Code/code_namespace.ML	Wed Nov 26 20:05:34 2014 +0100
   164.3 @@ -384,7 +384,7 @@
   164.4          val (name_fragments_common, (diff, diff')) =
   164.5            chop_prefix (op =) (name_fragments, name_fragments');
   164.6          val is_cross_module = not (null diff andalso null diff');
   164.7 -        val dep = pairself hd (map Code_Symbol.Module diff @ [sym], map Code_Symbol.Module diff' @ [sym']);
   164.8 +        val dep = apply2 hd (map Code_Symbol.Module diff @ [sym], map Code_Symbol.Module diff' @ [sym']);
   164.9          val add_edge = if is_cross_module andalso not cyclic_modules
  164.10            then add_edge_acyclic_error (fn _ => "Dependency "
  164.11              ^ Code_Symbol.quote ctxt sym ^ " -> "
  164.12 @@ -407,7 +407,7 @@
  164.13            |> List.partition
  164.14                (fn sym => case Code_Symbol.Graph.get_node nodes sym
  164.15                  of (_, Module _) => true | _ => false)
  164.16 -          |> pairself (prioritize sym_priority)
  164.17 +          |> apply2 (prioritize sym_priority)
  164.18          fun declare namify sym (nsps, nodes) =
  164.19            let
  164.20              val (base, node) = Code_Symbol.Graph.get_node nodes sym;
   165.1 --- a/src/Tools/Code/code_preproc.ML	Wed Nov 26 16:55:43 2014 +0100
   165.2 +++ b/src/Tools/Code/code_preproc.ML	Wed Nov 26 20:05:34 2014 +0100
   165.3 @@ -267,7 +267,7 @@
   165.4    in
   165.5      AList.make (snd o Graph.get_node eqngr) (Graph.keys eqngr)
   165.6      |> (map o apfst) (Code.string_of_const thy)
   165.7 -    |> sort (string_ord o pairself fst)
   165.8 +    |> sort (string_ord o apply2 fst)
   165.9      |> map (fn (s, cert) => (Pretty.block o Pretty.fbreaks) (Pretty.str s :: Code.pretty_cert thy cert))
  165.10      |> Pretty.chunks
  165.11    end;
   166.1 --- a/src/Tools/Code/code_target.ML	Wed Nov 26 16:55:43 2014 +0100
   166.2 +++ b/src/Tools/Code/code_target.ML	Wed Nov 26 20:05:34 2014 +0100
   166.3 @@ -117,11 +117,11 @@
   166.4  
   166.5  fun cert_syms ctxt =
   166.6    Code_Symbol.map_attr (apfst (cert_const ctxt)) (apfst (cert_tyco ctxt))
   166.7 -    (apfst (cert_class ctxt)) ((apfst o pairself) (cert_class ctxt)) (apfst (cert_inst ctxt)) I;
   166.8 +    (apfst (cert_class ctxt)) ((apfst o apply2) (cert_class ctxt)) (apfst (cert_inst ctxt)) I;
   166.9  
  166.10  fun read_syms ctxt =
  166.11    Code_Symbol.map_attr (apfst (read_const ctxt)) (apfst (read_tyco ctxt))
  166.12 -    (apfst (Proof_Context.read_class ctxt)) ((apfst o pairself) (Proof_Context.read_class ctxt)) (apfst (read_inst ctxt)) I;
  166.13 +    (apfst (Proof_Context.read_class ctxt)) ((apfst o apply2) (Proof_Context.read_class ctxt)) (apfst (read_inst ctxt)) I;
  166.14  
  166.15  fun check_name is_module s =
  166.16    let
   167.1 --- a/src/Tools/Code/code_thingol.ML	Wed Nov 26 16:55:43 2014 +0100
   167.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Nov 26 20:05:34 2014 +0100
   167.3 @@ -305,7 +305,7 @@
   167.4        ((v, ty) `|=> map_terms_bottom_up f t)
   167.5    | map_terms_bottom_up f (ICase { term = t, typ = ty, clauses = clauses, primitive = t0 }) = f
   167.6        (ICase { term = map_terms_bottom_up f t, typ = ty,
   167.7 -        clauses = (map o pairself) (map_terms_bottom_up f) clauses,
   167.8 +        clauses = (map o apply2) (map_terms_bottom_up f) clauses,
   167.9          primitive = map_terms_bottom_up f t0 });
  167.10  
  167.11  fun map_classparam_instances_as_term f =
  167.12 @@ -889,7 +889,7 @@
  167.13            then ([], consts_of_select (Context.this_theory thy (unsuffix "._" s)))
  167.14            else ([Code.read_const thy str], [])
  167.15        | NONE => ([Code.read_const thy str], []));
  167.16 -  in pairself flat o split_list o map read_const_expr end;
  167.17 +  in apply2 flat o split_list o map read_const_expr end;
  167.18  
  167.19  fun read_const_exprs_all ctxt = op @ o read_const_exprs_internal ctxt;
  167.20  
   168.1 --- a/src/Tools/Spec_Check/output_style.ML	Wed Nov 26 16:55:43 2014 +0100
   168.2 +++ b/src/Tools/Spec_Check/output_style.ML	Wed Nov 26 20:05:34 2014 +0100
   168.3 @@ -24,7 +24,7 @@
   168.4          val countw = 20
   168.5          val allw = namew + resultw + countw + 2
   168.6  
   168.7 -        val maybe_sort = if sort_examples then sort (int_ord o pairself size) else I
   168.8 +        val maybe_sort = if sort_examples then sort (int_ord o apply2 size) else I
   168.9  
  168.10          fun result ({count = 0, ...}, _) _ = "dubious"
  168.11            | result (_ : Property.stats, badobjs) false = if null badobjs then "ok" else "FAILED"
   169.1 --- a/src/Tools/atomize_elim.ML	Wed Nov 26 16:55:43 2014 +0100
   169.2 +++ b/src/Tools/atomize_elim.ML	Wed Nov 26 20:05:34 2014 +0100
   169.3 @@ -30,7 +30,7 @@
   169.4  fun invert_perm pi =
   169.5        (pi @ subtract (op =) pi (0 upto (fold Integer.max pi 0)))
   169.6             |> map_index I
   169.7 -           |> sort (int_ord o pairself snd)
   169.8 +           |> sort (int_ord o apply2 snd)
   169.9             |> map fst
  169.10  
  169.11  (* rearrange_prems as a conversion *)
   170.1 --- a/src/Tools/cache_io.ML	Wed Nov 26 16:55:43 2014 +0100
   170.2 +++ b/src/Tools/cache_io.ML	Wed Nov 26 20:05:34 2014 +0100
   170.3 @@ -98,14 +98,14 @@
   170.4                else if i < p + len2 then (i+1, apsnd (cons line) xsp)
   170.5                else (i, xsp)
   170.6              val (out, err) =
   170.7 -              pairself rev (snd (File.fold_lines load cache_path (1, ([], []))))
   170.8 +              apply2 rev (snd (File.fold_lines load cache_path (1, ([], []))))
   170.9            in ((SOME {output = err, redirected_output = out, return_code = 0}, key), tab) end))
  170.10    end
  170.11  
  170.12  fun run_and_cache (Cache {path = cache_path, table}) key make_cmd str =
  170.13    let
  170.14      val {output = err, redirected_output=out, return_code} = run make_cmd str
  170.15 -    val (l1, l2) = pairself length (out, err)
  170.16 +    val (l1, l2) = apply2 length (out, err)
  170.17      val header = key ^ " " ^ string_of_int l1 ^ " " ^ string_of_int l2
  170.18      val lines = map (suffix "\n") (header :: out @ err)
  170.19  
   171.1 --- a/src/Tools/coherent.ML	Wed Nov 26 16:55:43 2014 +0100
   171.2 +++ b/src/Tools/coherent.ML	Wed Nov 26 20:05:34 2014 +0100
   171.3 @@ -81,7 +81,7 @@
   171.4          (valid_conj ctxt facts
   171.5             (Pattern.match (Proof_Context.theory_of ctxt) (t, u) env) ts
   171.6           handle Pattern.MATCH => Seq.empty))
   171.7 -          (Seq.of_list (sort (int_ord o pairself snd) (Net.unify_term facts t)));
   171.8 +          (Seq.of_list (sort (int_ord o apply2 snd) (Net.unify_term facts t)));
   171.9  
  171.10  (* Instantiate variables that only occur free in conlusion *)
  171.11  fun inst_extra_vars ctxt dom cs =
  171.12 @@ -115,7 +115,7 @@
  171.13  
  171.14  fun string_of_facts ctxt s facts =
  171.15    Pretty.string_of (Pretty.big_list s
  171.16 -    (map (Syntax.pretty_term ctxt) (map fst (sort (int_ord o pairself snd) (Net.content facts)))));
  171.17 +    (map (Syntax.pretty_term ctxt) (map fst (sort (int_ord o apply2 snd) (Net.content facts)))));
  171.18  
  171.19  fun valid ctxt rules goal dom facts nfacts nparams =
  171.20    let
   172.1 --- a/src/Tools/induct.ML	Wed Nov 26 16:55:43 2014 +0100
   172.2 +++ b/src/Tools/induct.ML	Wed Nov 26 20:05:34 2014 +0100
   172.3 @@ -297,7 +297,7 @@
   172.4      in (context', thm') end);
   172.5  
   172.6  fun del_att which =
   172.7 -  Thm.declaration_attribute (fn th => Data.map (which (pairself (fn rs =>
   172.8 +  Thm.declaration_attribute (fn th => Data.map (which (apply2 (fn rs =>
   172.9      fold Item_Net.remove (filter_rules rs th) rs))));
  172.10  
  172.11  fun add_casesT rule x = @{apply 4(1)} (apfst (Item_Net.update rule)) x;
   173.1 --- a/src/Tools/nbe.ML	Wed Nov 26 16:55:43 2014 +0100
   173.2 +++ b/src/Tools/nbe.ML	Wed Nov 26 20:05:34 2014 +0100
   173.3 @@ -64,7 +64,7 @@
   173.4      val lhs_rhs = case try Logic.dest_equals eqn
   173.5       of SOME lhs_rhs => lhs_rhs
   173.6        | _ => error ("Not an equation: " ^ Syntax.string_of_term_global thy eqn);
   173.7 -    val c_c' = case try (pairself (Axclass.unoverload_const thy o dest_Const)) lhs_rhs
   173.8 +    val c_c' = case try (apply2 (Axclass.unoverload_const thy o dest_Const)) lhs_rhs
   173.9       of SOME c_c' => c_c'
  173.10        | _ => error ("Not an equation with two constants: "
  173.11            ^ Syntax.string_of_term_global thy eqn);
   174.1 --- a/src/Tools/subtyping.ML	Wed Nov 26 16:55:43 2014 +0100
   174.2 +++ b/src/Tools/subtyping.ML	Wed Nov 26 20:05:34 2014 +0100
   174.3 @@ -196,7 +196,7 @@
   174.4        quote (Syntax.string_of_typ ctxt (Type (a, replicate (length Ts) dummyT)));
   174.5  
   174.6      fun unif (T1, T2) (env as (tye, _)) =
   174.7 -      (case pairself (`Type_Infer.is_paramT o Type_Infer.deref tye) (T1, T2) of
   174.8 +      (case apply2 (`Type_Infer.is_paramT o Type_Infer.deref tye) (T1, T2) of
   174.9          ((true, TVar (xi, S)), (_, T)) => assign xi T S env
  174.10        | ((_, T), (true, TVar (xi, S))) => assign xi T S env
  174.11        | ((_, Type (a, Ts)), (_, Type (b, Us))) =>
  174.12 @@ -348,7 +348,7 @@
  174.13  
  174.14      fun split_cs _ [] = ([], [])
  174.15        | split_cs f (c :: cs) =
  174.16 -          (case pairself f (fst c) of
  174.17 +          (case apply2 f (fst c) of
  174.18              (false, false) => apsnd (cons c) (split_cs f cs)
  174.19            | _ => apfst (cons c) (split_cs f cs));
  174.20  
  174.21 @@ -392,7 +392,7 @@
  174.22              val test_update = is_typeT orf is_freeT orf is_fixedvarT;
  174.23              val (ch, done') =
  174.24                done
  174.25 -              |> map (apfst (pairself (Type_Infer.deref tye')))
  174.26 +              |> map (apfst (apply2 (Type_Infer.deref tye')))
  174.27                |> (if not (null new) then rpair []  else split_cs test_update);
  174.28              val todo' = ch @ todo;
  174.29            in
  174.30 @@ -667,7 +667,8 @@
  174.31  
  174.32  fun gen_coercion ctxt err tye TU =
  174.33    let
  174.34 -    fun gen (T1, T2) = (case pairself (Type_Infer.deref tye) (T1, T2) of
  174.35 +    fun gen (T1, T2) =
  174.36 +      (case apply2 (Type_Infer.deref tye) (T1, T2) of
  174.37          (T1 as (Type (a, [])), T2 as (Type (b, []))) =>
  174.38              if a = b
  174.39              then mk_identity T1
  174.40 @@ -949,7 +950,7 @@
  174.41      val coercions = map (fst o the o Symreltab.lookup tab) path';
  174.42      val trans_co = singleton (Variable.polymorphic ctxt)
  174.43        (fold safe_app coercions (mk_identity dummyT));
  174.44 -    val (Ts, Us) = pairself (snd o Term.dest_Type) (Term.dest_funT (type_of trans_co))
  174.45 +    val (Ts, Us) = apply2 (snd o Term.dest_Type) (Term.dest_funT (type_of trans_co));
  174.46    in
  174.47      (trans_co, ((Ts, Us), coercions))
  174.48    end;
  174.49 @@ -1076,7 +1077,7 @@
  174.50  
  174.51      val type_space = Proof_Context.type_space ctxt;
  174.52      val tmaps =
  174.53 -      sort (Name_Space.extern_ord ctxt type_space o pairself #1)
  174.54 +      sort (Name_Space.extern_ord ctxt type_space o apply2 #1)
  174.55          (Symtab.dest (tmaps_of ctxt));
  174.56      fun show_map (c, (t, _)) =
  174.57        Pretty.block