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