src/HOL/Tools/Meson/meson.ML
changeset 59058 a78612c67ec0
parent 58963 26bf09b95dda
child 59164 ff40c53d1af9
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Wed Nov 26 16:55:43 2014 +0100
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Wed Nov 26 20:05:34 2014 +0100
     1.3 @@ -109,7 +109,7 @@
     1.4            val tenv =
     1.5              Pattern.first_order_match thy (tmB, tmA)
     1.6                                            (Vartab.empty, Vartab.empty) |> snd
     1.7 -          val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
     1.8 +          val ct_pairs = map (apply2 (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
     1.9        in  thA RS (cterm_instantiate ct_pairs thB)  end) () of
    1.10      SOME th => th
    1.11    | NONE => raise THM ("first_order_resolve", 0, [thA, thB]))
    1.12 @@ -594,7 +594,7 @@
    1.13    let
    1.14      fun pat t u =
    1.15        let
    1.16 -        val ((head1, args1), (head2, args2)) = (t, u) |> pairself strip_comb
    1.17 +        val ((head1, args1), (head2, args2)) = (t, u) |> apply2 strip_comb
    1.18        in
    1.19          if head1 = head2 then
    1.20            let val pats = map2 pat args1 args2 in
    1.21 @@ -631,7 +631,7 @@
    1.22             $ (t as _ $ _) $ (u as _ $ _))) =>
    1.23      (case get_F_pattern T t u of
    1.24         SOME p =>
    1.25 -       let val inst = [pairself (cterm_of thy) (F_ext_cong_neq, p)] in
    1.26 +       let val inst = [apply2 (cterm_of thy) (F_ext_cong_neq, p)] in
    1.27           th RS cterm_instantiate inst ext_cong_neq
    1.28         end
    1.29       | NONE => th)