# HG changeset patch
# User wenzelm
# Date 1515674897 -3600
# Node ID e9ab4ad7bd15ee613df29425f7cbb7e04a13cd0d
# Parent  e128ab544996c956644b900a4627cc79b0248161
uniform use of Standard ML op-infix -- eliminated warnings;

diff -r e128ab544996 -r e9ab4ad7bd15 src/CTT/CTT.thy
--- a/src/CTT/CTT.thy	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/CTT/CTT.thy	Thu Jan 11 13:48:17 2018 +0100
@@ -434,7 +434,7 @@
 
 (*0 subgoals vs 1 or more*)
 val (safe0_brls, safep_brls) =
-    List.partition (curry (=) 0 o subgoals_of_brl) safe_brls
+    List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls
 
 fun safestep_tac ctxt thms i =
     form_tac ctxt ORELSE
diff -r e128ab544996 -r e9ab4ad7bd15 src/FOLP/IFOLP.thy
--- a/src/FOLP/IFOLP.thy	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/FOLP/IFOLP.thy	Thu Jan 11 13:48:17 2018 +0100
@@ -259,7 +259,7 @@
           and concl = discard_proof (Logic.strip_assums_concl prem)
       in
           if exists (fn hyp => hyp aconv concl) hyps
-          then case distinct (=) (filter (fn hyp => Term.could_unify (hyp, concl)) hyps) of
+          then case distinct (op =) (filter (fn hyp => Term.could_unify (hyp, concl)) hyps) of
                    [_] => assume_tac ctxt i
                  |  _  => no_tac
           else no_tac
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Bali/AxExample.thy
--- a/src/HOL/Bali/AxExample.thy	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Bali/AxExample.thy	Thu Jan 11 13:48:17 2018 +0100
@@ -42,7 +42,7 @@
 
 ML \<open>
 fun inst1_tac ctxt s t xs st =
-  (case AList.lookup (=) (rev (Term.add_var_names (Thm.prop_of st) [])) s of
+  (case AList.lookup (op =) (rev (Term.add_var_names (Thm.prop_of st) [])) s of
     SOME i => PRIMITIVE (Rule_Insts.read_instantiate ctxt [(((s, i), Position.none), t)] xs) st
   | NONE => Seq.empty);
 
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/HOL.thy	Thu Jan 11 13:48:17 2018 +0100
@@ -1607,7 +1607,7 @@
     type T = ((term -> bool) * stamp) list;
     val empty = [];
     val extend = I;
-    fun merge data : T = Library.merge (eq_snd (=)) data;
+    fun merge data : T = Library.merge (eq_snd (op =)) data;
   );
   fun add m = Data.map (cons (m, stamp ()));
   fun matches thy t = exists (fn (m, _) => m t) (Data.get thy);
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Library/Countable.thy
--- a/src/HOL/Library/Countable.thy	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Library/Countable.thy	Thu Jan 11 13:48:17 2018 +0100
@@ -180,7 +180,7 @@
         val pred_names = #names (fst induct_info)
         val induct_thms = #inducts (snd induct_info)
         val alist = pred_names ~~ induct_thms
-        val induct_thm = the (AList.lookup (=) alist pred_name)
+        val induct_thm = the (AList.lookup (op =) alist pred_name)
         val vars = rev (Term.add_vars (Thm.prop_of induct_thm) [])
         val insts = vars |> map (fn (_, T) => try (Thm.cterm_of ctxt)
           (Const (@{const_name Countable.finite_item}, T)))
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Library/Pattern_Aliases.thy
--- a/src/HOL/Library/Pattern_Aliases.thy	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Library/Pattern_Aliases.thy	Thu Jan 11 13:48:17 2018 +0100
@@ -60,7 +60,7 @@
   | SOME (var, t) => apfst (cons var) (strip_all t)
 
 fun all_Frees t =
-  fold_aterms (fn Free (x, t) => insert (=) (x, t) | _ => I) t []
+  fold_aterms (fn Free (x, t) => insert (op =) (x, t) | _ => I) t []
 
 fun subst_once (old, new) t =
   let
@@ -120,7 +120,7 @@
 
         val res = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs', rhs'))
 
-        val frees = filter (member (=) vars) (all_Frees res)
+        val frees = filter (member (op =) vars) (all_Frees res)
       in fold (fn v => Logic.dependent_all_name ("", v)) (map Free frees) res end
   | _ => t
 
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Library/refute.ML
--- a/src/HOL/Library/refute.ML	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Library/refute.ML	Thu Jan 11 13:48:17 2018 +0100
@@ -344,7 +344,7 @@
     val maxtime = read_int (allparams, "maxtime")
     val satsolver = read_string (allparams, "satsolver")
     val no_assms = read_bool (allparams, "no_assms")
-    val expect = the_default "" (AList.lookup (=) allparams "expect")
+    val expect = the_default "" (AList.lookup (op =) allparams "expect")
     (* all remaining parameters of the form "string=int" are collected in *)
     (* 'sizes'                                                            *)
     (* TODO: it is currently not possible to specify a size for a type    *)
@@ -1053,7 +1053,7 @@
             val fm_ax = Prop_Logic.all (map toTrue (tl intrs))
             val fm = Prop_Logic.all [#wellformed args, fm_ax, fm_u]
             val _ =
-              (if member (=) ["cdclite"] satsolver andalso Context_Position.is_visible ctxt then
+              (if member (op =) ["cdclite"] satsolver andalso Context_Position.is_visible ctxt then
                 warning ("Using SAT solver " ^ quote satsolver ^
                          "; for better performance, consider installing an \
                          \external solver.")
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Matrix_LP/Cplex_tools.ML
--- a/src/HOL/Matrix_LP/Cplex_tools.ML	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Matrix_LP/Cplex_tools.ML	Thu Jan 11 13:48:17 2018 +0100
@@ -969,10 +969,10 @@
     val header = readHeader ()
 
     val result =
-        case AList.lookup (=) header "STATUS" of
+        case AList.lookup (op =) header "STATUS" of
         SOME "INFEASIBLE" => Infeasible
           | SOME "UNBOUNDED" => Unbounded
-          | SOME "OPTIMAL" => Optimal (the (AList.lookup (=) header "OBJECTIVE"),
+          | SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) header "OBJECTIVE"),
                        (skip_until_sep ();
                         skip_until_sep ();
                         load_values ()))
@@ -1115,10 +1115,10 @@
     val header = readHeader ()
 
     val result =
-        case AList.lookup (=) header "STATUS" of
+        case AList.lookup (op =) header "STATUS" of
         SOME "INFEASIBLE" => Infeasible
           | SOME "NONOPTIMAL" => Unbounded
-          | SOME "OPTIMAL" => Optimal (the (AList.lookup (=) header "OBJECTIVE"),
+          | SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) header "OBJECTIVE"),
                        (skip_paragraph ();
                         skip_paragraph ();
                         skip_paragraph ();
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML	Thu Jan 11 13:48:17 2018 +0100
@@ -12,7 +12,7 @@
 
 fun run args id ({pre, timeout, log, ...}: Mirabelle.run_args) =
   let
-    val has_valid_key = member (=) ["iterations", "size", "generator"] o fst
+    val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
     val quickcheck = Quickcheck.quickcheck (map (apsnd single) (filter has_valid_key args)) 1
   in
     (case Timeout.apply timeout quickcheck pre of
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Jan 11 13:48:17 2018 +0100
@@ -472,7 +472,7 @@
     val e_selection_heuristic = AList.lookup (op =) args e_selection_heuristicK
     val term_order = AList.lookup (op =) args term_orderK
     val force_sos = AList.lookup (op =) args force_sosK
-      |> Option.map (curry (<>) "false")
+      |> Option.map (curry (op <>) "false")
     val dir = AList.lookup (op =) args keepK
     val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30)
     (* always use a hard timeout, but give some slack so that the automatic
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Nitpick_Examples/Mono_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Thu Jan 11 13:48:17 2018 +0100
@@ -160,7 +160,7 @@
   let
     fun is_type_actually_monotonic T =
       Nitpick_Mono.formulas_monotonic hol_ctxt binarize T tsp
-    val free_Ts = fold Term.add_tfrees ((@) tsp) [] |> map TFree
+    val free_Ts = fold Term.add_tfrees ((op @) tsp) [] |> map TFree
     val (mono_free_Ts, nonmono_free_Ts) =
       Timeout.apply mono_timeout
           (List.partition is_type_actually_monotonic) free_Ts
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Thu Jan 11 13:48:17 2018 +0100
@@ -1444,7 +1444,7 @@
     val big_rec_name = big_name ^ "_rec_set";
     val rec_set_names' =
       if length descr'' = 1 then [big_rec_name] else
-        map ((curry (^) (big_rec_name ^ "_")) o string_of_int)
+        map ((curry (op ^) (big_rec_name ^ "_")) o string_of_int)
           (1 upto (length descr''));
     val rec_set_names =  map (Sign.full_bname thy10) rec_set_names';
 
@@ -2030,7 +2030,7 @@
     val big_reccomb_name = space_implode "_" new_type_names ^ "_rec";
     val reccomb_names = map (Sign.full_bname thy11)
       (if length descr'' = 1 then [big_reccomb_name] else
-        (map ((curry (^) (big_reccomb_name ^ "_")) o string_of_int)
+        (map ((curry (op ^) (big_reccomb_name ^ "_")) o string_of_int)
           (1 upto (length descr''))));
     val reccombs = map (fn ((name, T), T') => list_comb
       (Const (name, rec_fn_Ts @ [T] ---> T'), rec_fns))
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML	Thu Jan 11 13:48:17 2018 +0100
@@ -45,7 +45,7 @@
     proc = fn _ => fn _ => fn ct =>
       (case Thm.term_of ct of
         Const (@{const_name Nominal.perm}, _) $ _ $ t =>
-          if member (=) names (the_default "" (try (head_of #> dest_Const #> fst) t))
+          if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
           then SOME perm_bool else NONE
       | _ => NONE)};
 
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Thu Jan 11 13:48:17 2018 +0100
@@ -49,7 +49,7 @@
     proc = fn _ => fn _ => fn ct =>
       (case Thm.term_of ct of
         Const (@{const_name Nominal.perm}, _) $ _ $ t =>
-          if member (=) names (the_default "" (try (head_of #> dest_Const #> fst) t))
+          if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
           then SOME perm_bool else NONE
        | _ => NONE)};
 
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Orderings.thy	Thu Jan 11 13:48:17 2018 +0100
@@ -473,7 +473,7 @@
 (* context data *)
 
 fun struct_eq ((s1: string, ts1), (s2, ts2)) =
-  s1 = s2 andalso eq_list (aconv) (ts1, ts2);
+  s1 = s2 andalso eq_list (op aconv) (ts1, ts2);
 
 structure Data = Generic_Data
 (
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Proofs/ex/Proof_Terms.thy
--- a/src/HOL/Proofs/ex/Proof_Terms.thy	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Proofs/ex/Proof_Terms.thy	Thu Jan 11 13:48:17 2018 +0100
@@ -35,7 +35,7 @@
   (*all theorems used in the graph of nested proofs*)
   val all_thms =
     Proofterm.fold_body_thms
-      (fn {name, ...} => insert (=) name) [body] [];
+      (fn {name, ...} => insert (op =) name) [body] [];
 \<close>
 
 text \<open>
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/SMT_Examples/boogie.ML
--- a/src/HOL/SMT_Examples/boogie.ML	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/SMT_Examples/boogie.ML	Thu Jan 11 13:48:17 2018 +0100
@@ -188,7 +188,7 @@
   let
     val ((Ts, atts), ls') =
       ls |> repeat (parse_type cx) arity ||>> repeat (parse_attr cx) n
-    val unique = member (=) atts "unique"
+    val unique = member (op =) atts "unique"
   in ((split_last Ts, unique), ls') end
 
 fun parse_decl (("type-decl" :: name :: _) :: ls) cx = (ls, add_type name cx)
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Thu Jan 11 13:48:17 2018 +0100
@@ -189,7 +189,7 @@
                    |> FIRST')
         val attempts = map instantiate parameters
       in
-        (fold (curry (APPEND')) attempts (K no_tac)) i st
+        (fold (curry (op APPEND')) attempts (K no_tac)) i st
       end
   end
 
@@ -227,7 +227,7 @@
       in
         if is_none quantified_var then no_tac st
         else
-          if member (=) parameters (the quantified_var |> fst) then
+          if member (op =) parameters (the quantified_var |> fst) then
             instantiates (the quantified_var |> fst) i st
           else
             K no_tac i st
@@ -664,7 +664,7 @@
               else
                 space_implode " " l
                 |> pair " "
-                |> (^))
+                |> (op ^))
 
   in
     if null gls orelse null candidate_consts then no_tac st
@@ -675,7 +675,7 @@
             @{thm leo2_skolemise}
         val attempts = map instantiate candidate_consts
       in
-        (fold (curry (APPEND')) attempts (K no_tac)) i st
+        (fold (curry (op APPEND')) attempts (K no_tac)) i st
       end
   end
 \<close>
@@ -799,7 +799,7 @@
   in
     map (strip_top_All_vars #> snd) conclusions
     |> maps (get_skolem_terms [] [])
-    |> distinct (=)
+    |> distinct (op =)
   end
 \<close>
 
@@ -827,9 +827,9 @@
             (*the parameters we will concern ourselves with*)
             val params' =
               Term.add_frees lhs []
-              |> distinct (=)
+              |> distinct (op =)
             (*check to make sure that params' <= params*)
-            val _ = @{assert} (forall (member (=) params) params')
+            val _ = @{assert} (forall (member (op =) params) params')
             val skolem_const_ty =
               let
                 val (skolem_const_prety, no_params) =
@@ -871,7 +871,7 @@
           val (arg_ty, val_ty) = Term.dest_funT cur_ty
           (*now find a param of type arg_ty*)
           val (candidate_param, params') =
-            find_and_remove (snd #> pair arg_ty #> (=)) params
+            find_and_remove (snd #> pair arg_ty #> (op =)) params
         in
           use_candidate target_ty params' (candidate_param :: acc) val_ty
         end
@@ -948,7 +948,7 @@
     val tactic =
       if is_none var_opt then no_tac
       else
-        fold (curry (APPEND))
+        fold (curry (op APPEND))
           (map (instantiate_tac (dest_Var (Thm.term_of (the var_opt)))) skolem_cts) no_tac
   in
     tactic st
@@ -1408,7 +1408,7 @@
         fold_options opt_list
         |> flat
         |> pair sought_sublist
-        |> subset (=)
+        |> subset (op =)
   in
     case x of
         CleanUp l' =>
@@ -1423,7 +1423,7 @@
       | InnerLoopOnce l' =>
           map sublist_of_inner_loop_once l
           |> check_sublist l'
-      | _ => exists (curry (=) x) l
+      | _ => exists (curry (op =) x) l
   end;
 
 fun loop_can_feature loop_feats l =
@@ -1586,7 +1586,7 @@
     fun extcnf_combined_tac' ctxt i = fn st =>
       let
         val skolem_consts_used_so_far = which_skolem_concs_used ctxt st
-        val consts_diff' = subtract (=) skolem_consts_used_so_far consts_diff
+        val consts_diff' = subtract (op =) skolem_consts_used_so_far consts_diff
 
         fun feat_to_tac feat =
           case feat of
@@ -1692,7 +1692,7 @@
       #> uncurry TPTP_Reconstruct.new_consts_between
       #> filter
            (fn Const (n, _) =>
-             not (member (=) interpreted_consts n))
+             not (member (op =) interpreted_consts n))
   in
     if head_of t = Logic.implies then do_diff t
     else []
@@ -1731,8 +1731,8 @@
             val (conc_prefix, conc_body) = sep_prefix conc_clause
           in
             if null hyp_prefix orelse
-              member (=) conc_prefix (hd hyp_prefix) orelse
-              member (=)  (Term.add_frees hyp_body []) (hd hyp_prefix) then
+              member (op =) conc_prefix (hd hyp_prefix) orelse
+              member (op =)  (Term.add_frees hyp_body []) (hd hyp_prefix) then
               no_tac st
             else
               Rule_Insts.eres_inst_tac ctxt [((("x", 0), Position.none), "(@X. False)")] []
@@ -1800,7 +1800,7 @@
                        |> apfst rev)
               in
                 if null hyp_lit_prefix orelse
-                  member (=)  (Term.add_frees hyp_lit_body []) (hd hyp_lit_prefix) then
+                  member (op =)  (Term.add_frees hyp_lit_body []) (hd hyp_lit_prefix) then
                   no_tac st
                 else
                   dresolve_tac ctxt @{thms drop_redundant_literal_qtfr} i st
@@ -2042,14 +2042,14 @@
        []
 
     val source_inf_opt =
-      AList.lookup (=) (#meta pannot)
+      AList.lookup (op =) (#meta pannot)
       #> the
       #> #source_inf_opt
 
     (*FIXME integrate this with other lookup code, or in the early analysis*)
     local
       fun node_is_of_role role node =
-        AList.lookup (=) (#meta pannot) node |> the
+        AList.lookup (op =) (#meta pannot) node |> the
         |> #role
         |> (fn role' => role = role')
 
@@ -2081,7 +2081,7 @@
                              map snd (values ())
                            end
                          else
-                         map (fn node => AList.lookup (=) (values ()) node |> the) x)
+                         map (fn node => AList.lookup (op =) (values ()) node |> the) x)
                 | _ => []
          end
 
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Thu Jan 11 13:48:17 2018 +0100
@@ -711,9 +711,9 @@
     val decls =
       func_decls @ pred_decls @ datatype_decls @ sort_decls @ subclass_decls
     val axioms =
-      filt (formula (curry (<>) Conjecture)) |> separate [""] |> flat
+      filt (formula (curry (op <>) Conjecture)) |> separate [""] |> flat
     val conjs =
-      filt (formula (curry (=) Conjecture)) |> separate [""] |> flat
+      filt (formula (curry (op =) Conjecture)) |> separate [""] |> flat
     val settings =
       (if is_lpo then ["set_flag(Ordering, 1)."] else []) @
       (if gen_prec then
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Jan 11 13:48:17 2018 +0100
@@ -1036,7 +1036,7 @@
   #> raw_mangled_const_name generic_mangled_type_name
 
 val parse_mangled_ident =
-  Scan.many1 (not o member (=) ["(", ")", ","]) >> implode
+  Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
 
 fun parse_mangled_type x =
   (parse_mangled_ident
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Tools/BNF/bnf_gfp.ML
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Jan 11 13:48:17 2018 +0100
@@ -549,12 +549,12 @@
       ||>> mk_Frees "s'" s'Ts
       ||>> mk_Frees "s''" s''Ts
       ||>> mk_Frees "f" fTs
-      ||>> yield_singleton (apfst (~~) oo mk_Frees' "Rtuple") all_sbisT
+      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "Rtuple") all_sbisT
       ||>> mk_Frees "R" setRTs
       ||>> mk_Frees "R" setRTs
       ||>> mk_Frees "R'" setR'Ts
       ||>> mk_Frees "R" setsRTs
-      ||>> yield_singleton (apfst (~~) oo mk_Frees' "i") idxT
+      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "i") idxT
       ||>> yield_singleton (mk_Frees "I") (HOLogic.mk_setT idxT)
       ||>> mk_Frees "Ri" (map (fn T => idxT --> T) setRTs);
 
@@ -831,17 +831,17 @@
       |> mk_Frees' "b" activeAs
       ||>> mk_Frees "b" activeAs
       ||>> mk_Frees "s" sTs
-      ||>> yield_singleton (apfst (~~) oo mk_Frees' "n") HOLogic.natT
-      ||>> yield_singleton (apfst (~~) oo mk_Frees' "sumx") sum_sbdT
+      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "n") HOLogic.natT
+      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "sumx") sum_sbdT
       ||>> mk_Frees' "k" sbdTs
-      ||>> yield_singleton (apfst (~~) oo mk_Frees' "kl") sum_sbd_listT
-      ||>> yield_singleton (apfst (~~) oo mk_Frees' "kl") sum_sbd_listT
-      ||>> yield_singleton (apfst (~~) oo mk_Frees' "Kl") sum_sbd_list_setT
-      ||>> yield_singleton (apfst (~~) oo mk_Frees' "lab") (sum_sbd_listT --> sbdFT)
-      ||>> yield_singleton (apfst (~~) oo mk_Frees' "Kl_lab") treeT
+      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "kl") sum_sbd_listT
+      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "kl") sum_sbd_listT
+      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "Kl") sum_sbd_list_setT
+      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "lab") (sum_sbd_listT --> sbdFT)
+      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "Kl_lab") treeT
       ||>> mk_Frees "x" bdFTs
-      ||>> yield_singleton (apfst (~~) oo mk_Frees' "rec") Lev_recT
-      ||>> yield_singleton (apfst (~~) oo mk_Frees' "rec") rv_recT;
+      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "rec") Lev_recT
+      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "rec") rv_recT;
 
     val (k, k') = (hd kks, hd kks')
 
@@ -1128,8 +1128,8 @@
       ||>> mk_Frees "b" activeAs
       ||>> mk_Frees "b" activeAs
       ||>> mk_Frees "s" sTs
-      ||>> yield_singleton (apfst (~~) oo mk_Frees' "n") HOLogic.natT
-      ||>> yield_singleton (apfst (~~) oo mk_Frees' "kl") sum_sbd_listT;
+      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "n") HOLogic.natT
+      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "kl") sum_sbd_listT;
 
     val (length_Lev_thms, length_Lev'_thms) =
       let
@@ -1687,7 +1687,7 @@
         val uTs = map2 (curry op -->) Ts Ts';
         val (((((nat, nat'), (Jzs, Jzs')), (hrecs, hrecs')), (fs, fs')), _) =
           lthy
-          |> yield_singleton (apfst (~~) oo mk_Frees' "n") HOLogic.natT
+          |> yield_singleton (apfst (op ~~) oo mk_Frees' "n") HOLogic.natT
           ||>> mk_Frees' "z" Ts
           ||>> mk_Frees' "rec" hrecTs
           ||>> mk_Frees' "f" fTs;
@@ -1798,7 +1798,7 @@
             (Jys, Jys')), (Jys_copy, Jys'_copy)), (ys_copy, ys'_copy)), Kss), names_lthy) =
           lthy
           |> mk_Frees' "y" passiveAs
-          ||>> yield_singleton (apfst (~~) oo mk_Frees' "n") HOLogic.natT
+          ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "n") HOLogic.natT
           ||>> mk_Frees' "z" Ts
           ||>> mk_Frees "y" Ts'
           ||>> mk_Frees "z'" Ts
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Tools/BNF/bnf_lfp.ML
--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Jan 11 13:48:17 2018 +0100
@@ -537,8 +537,8 @@
       ||>> mk_Frees "s" sTs
       ||>> mk_Frees "i" (replicate n suc_bdT)
       ||>> (fn ctxt => apfst the_single (mk_fresh_names ctxt 1 "Asi"))
-      ||>> yield_singleton (apfst (~~) oo mk_Frees' "i") suc_bdT
-      ||>> yield_singleton (apfst (~~) oo mk_Frees' "j") suc_bdT;
+      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "i") suc_bdT
+      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "j") suc_bdT;
 
     val suc_bd_limit_thm =
       let
@@ -764,7 +764,7 @@
       lthy
       |> mk_Frees "IIB" II_BTs
       ||>> mk_Frees "IIs" II_sTs
-      ||>> yield_singleton (apfst (~~) oo mk_Frees' "i") IIT
+      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "i") IIT
       ||>> mk_Frees "x" init_FTs;
 
     val II = HOLogic.mk_Collect (fst iidx', IIT, list_exists_free (II_Bs @ II_ss)
@@ -816,7 +816,7 @@
       |> mk_Frees "B" BTs
       ||>> mk_Frees "s" sTs
       ||>> mk_Frees "f" (map (fn T => Asuc_bdT --> T) activeAs)
-      ||>> yield_singleton (apfst (~~) oo mk_Frees' "i") IIT
+      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "i") IIT
       ||>> mk_Frees "ix" active_initTs
       ||>> mk_Frees' "x" init_FTs
       ||>> mk_Frees "f" init_fTs
@@ -941,7 +941,7 @@
     val ((ss, (fold_f, fold_f')), _) =
       lthy
       |> mk_Frees "s" sTs
-      ||>> yield_singleton (apfst (~~) oo mk_Frees' "f") foldT;
+      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "f") foldT;
 
     fun ctor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctorN ^ "_");
     val ctor_def_bind = rpair [] o Binding.concealed o Thm.def_binding o ctor_bind;
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Jan 11 13:48:17 2018 +0100
@@ -477,7 +477,7 @@
       ||>> mk_Frees "f" case_Ts
       ||>> mk_Frees "g" case_Ts
       ||>> yield_singleton (mk_Frees "z") B
-      ||>> yield_singleton (apfst (~~) oo mk_Frees' "P") HOLogic.boolT;
+      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT;
 
     val q = Free (fst p', mk_pred1T B);
 
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Tools/Nitpick/nitpick_commands.ML
--- a/src/HOL/Tools/Nitpick/nitpick_commands.ML	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML	Thu Jan 11 13:48:17 2018 +0100
@@ -96,7 +96,7 @@
 fun is_known_raw_param s =
   AList.defined (op =) default_default_params s orelse
   AList.defined (op =) negated_params s orelse
-  member (=) ["max", "show_all", "whack", "eval", "need", "atoms",
+  member (op =) ["max", "show_all", "whack", "eval", "need", "atoms",
                  "expect"] s orelse
   exists (fn p => String.isPrefix (p ^ " ") s)
          ["card", "max", "iter", "box", "dont_box", "finitize", "dont_finitize",
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Jan 11 13:48:17 2018 +0100
@@ -574,7 +574,7 @@
         (* use the first ML solver (to avoid startup overhead) *)
         val (ml_solvers, nonml_solvers) =
           SAT_Solver.get_solvers ()
-          |> List.partition (member (=) ["dptsat", "cdclite"] o fst)
+          |> List.partition (member (op =) ["dptsat", "cdclite"] o fst)
         val res =
           if null nonml_solvers then
             Timeout.apply tac_timeout (snd (hd ml_solvers)) prop
@@ -604,7 +604,7 @@
   string_for_mtype (nth Ms (length Ms - j - 1))
 
 fun string_for_free relevant_frees ((s, _), M) =
-  if member (=) relevant_frees s then SOME (s ^ " : " ^ string_for_mtype M)
+  if member (op =) relevant_frees s then SOME (s ^ " : " ^ string_for_mtype M)
   else NONE
 
 fun string_for_mcontext ctxt t ({bound_Ms, frame, frees, ...} : mcontext) =
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Tools/Nunchaku/nunchaku_collect.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku_collect.ML	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_collect.ML	Thu Jan 11 13:48:17 2018 +0100
@@ -530,7 +530,7 @@
     val def = specialize_type thy x def0;
     val lhs = lhs_of_equation def;
   in
-    if exists_Const (curry (=) x) lhs then def else raise Fail "cannot specialize"
+    if exists_Const (curry (op =) x) lhs then def else raise Fail "cannot specialize"
   end;
 
 fun definition_of thy (x as (s, _)) =
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Tools/Nunchaku/nunchaku_commands.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku_commands.ML	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_commands.ML	Thu Jan 11 13:48:17 2018 +0100
@@ -56,7 +56,7 @@
   AList.defined (op =) default_default_params s orelse
   AList.defined (op =) alias_params s orelse
   AList.defined (op =) negated_alias_params s orelse
-  member (=) ["atoms", "card", "eval", "expect"] s orelse
+  member (op =) ["atoms", "card", "eval", "expect"] s orelse
   exists (fn p => String.isPrefix (p ^ " ") s)
     ["atoms", "card", "dont_whack", "mono", "non_mono", "non_wf", "wf", "whack"];
 
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Tools/Nunchaku/nunchaku_reconstruct.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku_reconstruct.ML	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_reconstruct.ML	Thu Jan 11 13:48:17 2018 +0100
@@ -52,7 +52,7 @@
 
 val nun_arrow_exploded = String.explode nun_arrow;
 
-val is_ty_meta = member (=) (String.explode "()->,");
+val is_ty_meta = member (op =) (String.explode "()->,");
 
 fun next_token_lowlevel [] = (End_of_Stream, [])
   | next_token_lowlevel (c :: cs) =
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Jan 11 13:48:17 2018 +0100
@@ -603,7 +603,7 @@
       | has_positive_recursive_prems _ = false
     fun mk_lim_prem (Conj prems) = Conj (map mk_lim_prem prems)
       | mk_lim_prem (p as Rel (rel, ts)) =
-        if member (=) rel_names rel then Rel (mk_lim_rel_name rel, Var "Lim" :: ts) else p
+        if member (op =) rel_names rel then Rel (mk_lim_rel_name rel, Var "Lim" :: ts) else p
       | mk_lim_prem p = p
   in
     if has_positive_recursive_prems prem then
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Tools/Predicate_Compile/core_data.ML
--- a/src/HOL/Tools/Predicate_Compile/core_data.ML	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Tools/Predicate_Compile/core_data.ML	Thu Jan 11 13:48:17 2018 +0100
@@ -301,7 +301,7 @@
   in
     fold Term.add_const_names intros []
       |> (fn cs =>
-        if member (=) cs @{const_name "HOL.eq"} then
+        if member (op =) cs @{const_name "HOL.eq"} then
           insert (op =) @{const_name Predicate.eq} cs
         else cs)
       |> filter (fn c => (not (c = key)) andalso
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Jan 11 13:48:17 2018 +0100
@@ -1034,7 +1034,7 @@
     val process =
       rewrite_rule ctxt (Named_Theorems.get ctxt @{named_theorems code_pred_simp})
     fun process_False intro_t =
-      if member (=) (Logic.strip_imp_prems intro_t) @{prop "False"}
+      if member (op =) (Logic.strip_imp_prems intro_t) @{prop "False"}
       then NONE else SOME intro_t
     fun process_True intro_t =
       map_filter_premises (fn p => if p = @{prop True} then NONE else SOME p) intro_t
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML	Thu Jan 11 13:48:17 2018 +0100
@@ -765,7 +765,7 @@
   if not (member (op =) [HOLogic.intT, HOLogic.natT, HOLogic.boolT] (Thm.typ_of_cterm t))
   then false 
   else case Thm.term_of t of 
-    c$l$r => if member (=) [@{term"( * )::int => _"}, @{term"( * )::nat => _"}] c
+    c$l$r => if member (op =) [@{term"( * )::int => _"}, @{term"( * )::nat => _"}] c
              then not (isnum l orelse isnum r)
              else not (member (op aconv) cts c)
   | c$_ => not (member (op aconv) cts c)
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Tools/SMT/smt_systems.ML
--- a/src/HOL/Tools/SMT/smt_systems.ML	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Tools/SMT/smt_systems.ML	Thu Jan 11 13:48:17 2018 +0100
@@ -37,7 +37,7 @@
   in (test_outcome solver_name l, ls) end
 
 fun on_first_non_unsupported_line test_outcome solver_name lines =
-  on_first_line test_outcome solver_name (filter (curry (<>) "unsupported") lines)
+  on_first_line test_outcome solver_name (filter (curry (op <>) "unsupported") lines)
 
 (* CVC3 *)
 
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Tools/SMT/smtlib.ML
--- a/src/HOL/Tools/SMT/smtlib.ML	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Tools/SMT/smtlib.ML	Thu Jan 11 13:48:17 2018 +0100
@@ -67,7 +67,7 @@
 
 (* hex numbers *)
 
-val is_hex = member (=) (raw_explode "0123456789abcdefABCDEF")
+val is_hex = member (op =) (raw_explode "0123456789abcdefABCDEF")
 
 fun within c1 c2 c = (ord c1 <= ord c andalso ord c <= ord c2)
 
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Tools/SMT/smtlib_interface.ML
--- a/src/HOL/Tools/SMT/smtlib_interface.ML	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Thu Jan 11 13:48:17 2018 +0100
@@ -146,7 +146,7 @@
 
 fun serialize smt_options comments {logic, sorts, dtyps, funcs} ts =
   let
-    val unsat_core = member (=) smt_options (":produce-unsat-cores", "true")
+    val unsat_core = member (op =) smt_options (":produce-unsat-cores", "true")
   in
     Buffer.empty
     |> fold (Buffer.add o enclose "; " "\n") comments
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Thu Jan 11 13:48:17 2018 +0100
@@ -98,7 +98,7 @@
   AList.defined (op =) default_default_params s orelse
   AList.defined (op =) alias_params s orelse
   AList.defined (op =) negated_alias_params s orelse
-  member (=) property_dependent_params s orelse s = "expect"
+  member (op =) property_dependent_params s orelse s = "expect"
 
 fun is_prover_list ctxt s =
   (case space_explode " " s of
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Thu Jan 11 13:48:17 2018 +0100
@@ -284,15 +284,15 @@
     fun of_label l = if l = no_label then "" else string_of_label l ^ ": "
 
     fun of_obtain qs nr =
-      (if nr > 1 orelse (nr = 1 andalso member (=) qs Then) then "ultimately "
-       else if nr = 1 orelse member (=) qs Then then "then "
+      (if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then "ultimately "
+       else if nr = 1 orelse member (op =) qs Then then "then "
        else "") ^ "obtain"
 
-    fun of_show_have qs = if member (=) qs Show then "show" else "have"
-    fun of_thus_hence qs = if member (=) qs Show then "then show" else "then have"
+    fun of_show_have qs = if member (op =) qs Show then "show" else "have"
+    fun of_thus_hence qs = if member (op =) qs Show then "then show" else "then have"
 
     fun of_have qs nr =
-      if nr > 1 orelse (nr = 1 andalso member (=) qs Then) then "ultimately " ^ of_show_have qs
+      if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then "ultimately " ^ of_show_have qs
       else if nr = 1 orelse member (op =) qs Then then of_thus_hence qs
       else of_show_have qs
 
@@ -344,7 +344,7 @@
       end
     and of_subproofs _ _ _ [] = ""
       | of_subproofs ind ctxt qs subs =
-        (if member (=) qs Then then of_moreover ind else "") ^
+        (if member (op =) qs Then then of_moreover ind else "") ^
         space_implode (of_moreover ind) (map (of_subproof ind ctxt) subs)
     and add_step_pre ind qs subs (s, ctxt) =
       (s ^ of_subproofs ind ctxt qs subs ^ of_indent ind, ctxt)
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Tools/datatype_realizer.ML
--- a/src/HOL/Tools/datatype_realizer.ML	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML	Thu Jan 11 13:48:17 2018 +0100
@@ -34,7 +34,7 @@
       else map (fn i => "P" ^ string_of_int i) (1 upto length descr);
 
     val rec_result_Ts = map (fn ((i, _), P) =>
-        if member (=) is i then TFree ("'" ^ P, @{sort type}) else HOLogic.unitT)
+        if member (op =) is i then TFree ("'" ^ P, @{sort type}) else HOLogic.unitT)
       (descr ~~ pnames);
 
     fun make_pred i T U r x =
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Tools/functor.ML
--- a/src/HOL/Tools/functor.ML	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Tools/functor.ML	Thu Jan 11 13:48:17 2018 +0100
@@ -199,7 +199,7 @@
       | add_tycos _ = I;
     val tycos = add_tycos T [];
     val tyco = if tycos = ["fun"] then "fun"
-      else case remove (=) "fun" tycos
+      else case remove (op =) "fun" tycos
        of [tyco] => tyco
         | _ => error ("Bad number of type constructors: " ^ Syntax.string_of_typ ctxt T);
   in (mapper, T, tyco) end;
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Tools/groebner.ML
--- a/src/HOL/Tools/groebner.ML	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Tools/groebner.ML	Thu Jan 11 13:48:17 2018 +0100
@@ -601,7 +601,7 @@
     else tm::acc ;
 
 fun grobify_term vars tm =
-((if not (member (aconvc) vars tm) then raise CTERM ("Not a variable", [tm]) else
+((if not (member (op aconvc) vars tm) then raise CTERM ("Not a variable", [tm]) else
      [(@1, map (fn i => if i aconvc tm then 1 else 0) vars)])
 handle  CTERM _ =>
  ((let val x = dest_const tm
@@ -823,7 +823,7 @@
   val th1 = (the (get_first (try (isolate_variable vars)) cjs)
              handle Option.Option => raise CTERM ("unwind_polys_conv",[tm]))
   val eq = Thm.lhs_of th1
-  val bod' = list_mk_binop \<^cterm>\<open>HOL.conj\<close> (eq::(remove (aconvc) eq cjs))
+  val bod' = list_mk_binop \<^cterm>\<open>HOL.conj\<close> (eq::(remove (op aconvc) eq cjs))
   val th2 = conj_ac_rule (mk_eq bod bod')
   val th3 =
     Thm.transitive th2
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Tools/sat_solver.ML
--- a/src/HOL/Tools/sat_solver.ML	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Tools/sat_solver.ML	Thu Jan 11 13:48:17 2018 +0100
@@ -339,7 +339,7 @@
     o (map (map literal_from_int))
     o clauses
     o (map int_from_string)
-    o (maps (String.tokens (member (=) [#" ", #"\t", #"\n"])))
+    o (maps (String.tokens (member (op =) [#" ", #"\t", #"\n"])))
     o filter_preamble
     o filter (fn l => l <> "")
     o split_lines
diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Word/WordBitwise.thy
--- a/src/HOL/Word/WordBitwise.thy	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Word/WordBitwise.thy	Thu Jan 11 13:48:17 2018 +0100
@@ -479,7 +479,7 @@
       Goal.prove_internal ctxt [] (propfn I)
         (K (simp_tac (put_simpset word_ss ctxt) 1));
   in
-    Goal.prove_internal ctxt [] (propfn (curry ($) f))
+    Goal.prove_internal ctxt [] (propfn (curry (op $) f))
       (K (simp_tac (put_simpset HOL_ss ctxt addsimps [eq1]) 1))
     |> mk_meta_eq |> SOME
   end handle TERM _ => NONE;
@@ -529,7 +529,7 @@
   let
     val (ss, sss) = expand_word_eq_sss;
   in
-    foldr1 (THEN_ALL_NEW)
+    foldr1 (op THEN_ALL_NEW)
       ((CHANGED o safe_full_simp_tac (put_simpset ss ctxt)) ::
         map (fn ss => safe_full_simp_tac (put_simpset ss ctxt)) sss)
   end;