--- 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)