src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 59058 a78612c67ec0
parent 59049 0d1bfc982501
child 59580 cbc38731d42f
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Nov 26 16:55:43 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Nov 26 20:05:34 2014 +0100
     1.3 @@ -74,7 +74,7 @@
     1.4      val nesting_bnfss =
     1.5        map (fn sugar => #fp_nesting_bnfs sugar @ #live_nesting_bnfs sugar) fp_sugars;
     1.6      val fp_or_nesting_bnfss = fp_bnfs :: nesting_bnfss;
     1.7 -    val fp_or_nesting_bnfs = distinct (op = o pairself T_of_bnf) (flat fp_or_nesting_bnfss);
     1.8 +    val fp_or_nesting_bnfs = distinct (op = o apply2 T_of_bnf) (flat fp_or_nesting_bnfss);
     1.9  
    1.10      val fp_absTs = map #absT fp_absT_infos;
    1.11      val fp_repTs = map #repT fp_absT_infos;
    1.12 @@ -139,7 +139,7 @@
    1.13      val rels =
    1.14        let
    1.15          fun find_rel T As Bs = fp_or_nesting_bnfss
    1.16 -          |> map (filter_out (curry (op = o pairself name_of_bnf) BNF_Comp.DEADID_bnf))
    1.17 +          |> map (filter_out (curry (op = o apply2 name_of_bnf) BNF_Comp.DEADID_bnf))
    1.18            |> get_first (find_first (fn bnf => Type.could_unify (T_of_bnf bnf, T)))
    1.19            |> Option.map (fn bnf =>
    1.20              let val live = live_of_bnf bnf;
    1.21 @@ -191,7 +191,7 @@
    1.22            case_fp fp (snd o Term.dest_comb) (snd o Term.dest_comb o fst o Term.dest_comb);
    1.23          val raw_phis = map (extract o HOLogic.dest_Trueprop o Thm.concl_of) rel_xtor_co_inducts;
    1.24          val thetas = AList.group (op =)
    1.25 -          (mutual_cliques ~~ map (pairself (certify lthy)) (raw_phis ~~ pre_phis));
    1.26 +          (mutual_cliques ~~ map (apply2 (certify lthy)) (raw_phis ~~ pre_phis));
    1.27        in
    1.28          map2 (Drule.cterm_instantiate o the o AList.lookup (op =) thetas)
    1.29          mutual_cliques rel_xtor_co_inducts
    1.30 @@ -286,7 +286,7 @@
    1.31  
    1.32          val fold_pre_deads_only_Ts =
    1.33            map (typ_subst_nonatomic_sorted (map (rpair dummyT)
    1.34 -            (As @ sort (int_ord o pairself Term.size_of_typ) fpTs))) fold_preTs';
    1.35 +            (As @ sort (int_ord o apply2 Term.size_of_typ) fpTs))) fold_preTs';
    1.36  
    1.37          val (mutual_clique, TUs) =
    1.38            map_split dest_co_algT (binder_fun_types (foldT_of_recT (fastype_of approx_rec)))
    1.39 @@ -439,7 +439,7 @@
    1.40            @{thms fst_convol map_prod_o_convol convol_o fst_comp_map_prod}
    1.41            @{thms case_sum_o_inj(1) case_sum_o_map_sum o_case_sum map_sum_o_inj(1)};
    1.42  
    1.43 -        val eq_thm_prop_untyped = Term.aconv_untyped o pairself Thm.full_prop_of;
    1.44 +        val eq_thm_prop_untyped = Term.aconv_untyped o apply2 Thm.full_prop_of;
    1.45  
    1.46          val map_thms = no_refl (maps (fn bnf =>
    1.47             let val map_comp0 = map_comp0_of_bnf bnf RS sym