src/HOL/Nominal/nominal_inductive.ML
changeset 59058 a78612c67ec0
parent 58112 8081087096ad
child 59498 50b60f501b05
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Wed Nov 26 16:55:43 2014 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Wed Nov 26 20:05:34 2014 +0100
     1.3 @@ -62,7 +62,7 @@
     1.4                   in (add_binders thy i u
     1.5                     (fold (fn (u, T) =>
     1.6                        if exists (fn j => j < i) (loose_bnos u) then I
     1.7 -                      else insert (op aconv o pairself fst)
     1.8 +                      else insert (op aconv o apply2 fst)
     1.9                          (incr_boundvars (~i) u, T)) cargs1 bs'), cargs2)
    1.10                   end) cargs (bs, ts ~~ Ts))))
    1.11        | _ => fold (add_binders thy i) ts bs)
    1.12 @@ -164,7 +164,7 @@
    1.13        HOLogic.dest_conj |> map (HOLogic.dest_imp ##> strip_comb);
    1.14      val ps = map (fst o snd) concls;
    1.15  
    1.16 -    val _ = (case duplicates (op = o pairself fst) avoids of
    1.17 +    val _ = (case duplicates (op = o apply2 fst) avoids of
    1.18          [] => ()
    1.19        | xs => error ("Duplicate case names: " ^ commas_quote (map fst xs)));
    1.20      val _ = avoids |> forall (fn (a, xs) => null (duplicates (op =) xs) orelse
    1.21 @@ -338,7 +338,7 @@
    1.22                   val pis'' = fold (concat_perm #> map) pis' pis;
    1.23                   val env = Pattern.first_order_match thy (ihypt, prop_of ihyp)
    1.24                     (Vartab.empty, Vartab.empty);
    1.25 -                 val ihyp' = Thm.instantiate ([], map (pairself (cterm_of thy))
    1.26 +                 val ihyp' = Thm.instantiate ([], map (apply2 (cterm_of thy))
    1.27                     (map (Envir.subst_term env) vs ~~
    1.28                      map (fold_rev (NominalDatatype.mk_perm [])
    1.29                        (rev pis' @ pis)) params' @ [z])) ihyp;