src/Pure/Proof/extraction.ML
changeset 59058 a78612c67ec0
parent 58950 d07464875dd4
child 59582 0fbed69ff081
     1.1 --- a/src/Pure/Proof/extraction.ML	Wed Nov 26 16:55:43 2014 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Wed Nov 26 20:05:34 2014 +0100
     1.3 @@ -103,14 +103,14 @@
     1.4            fun ren t = the_default t (Term.rename_abs tm1 tm t);
     1.5            val inc = Logic.incr_indexes ([], maxidx_of_term tm + 1);
     1.6            val env as (Tenv, tenv) = Pattern.match thy (inc tm1, tm) (Vartab.empty, Vartab.empty);
     1.7 -          val prems' = map (pairself (Envir.subst_term env o inc o ren)) prems;
     1.8 +          val prems' = map (apply2 (Envir.subst_term env o inc o ren)) prems;
     1.9            val env' = Envir.Envir
    1.10              {maxidx = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u) prems' ~1,
    1.11               tenv = tenv, tyenv = Tenv};
    1.12 -          val env'' = fold (Pattern.unify (Context.Theory thy) o pairself (lookup rew)) prems' env';
    1.13 +          val env'' = fold (Pattern.unify (Context.Theory thy) o apply2 (lookup rew)) prems' env';
    1.14          in SOME (Envir.norm_term env'' (inc (ren tm2)))
    1.15          end handle Pattern.MATCH => NONE | Pattern.Unif => NONE)
    1.16 -          (sort (int_ord o pairself fst)
    1.17 +          (sort (int_ord o apply2 fst)
    1.18              (Net.match_term rules (Envir.eta_contract tm)))
    1.19        end;
    1.20  
    1.21 @@ -207,7 +207,7 @@
    1.22      {realizes_eqns = merge_rules realizes_eqns1 realizes_eqns2,
    1.23       typeof_eqns = merge_rules typeof_eqns1 typeof_eqns2,
    1.24       types = AList.merge (op =) (K true) (types1, types2),
    1.25 -     realizers = Symtab.merge_list (eq_set (op =) o pairself #1) (realizers1, realizers2),
    1.26 +     realizers = Symtab.merge_list (eq_set (op =) o apply2 #1) (realizers1, realizers2),
    1.27       defs = Library.merge Thm.eq_thm (defs1, defs2),
    1.28       expand = Library.merge (op =) (expand1, expand2),
    1.29       prep = if is_some prep1 then prep1 else prep2};