--- 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
--- 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
--- 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);
--- 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);
--- 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)))
--- 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
--- 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.")
--- 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 ();
--- 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
--- 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
--- 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
--- 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))
--- 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)};
--- 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)};
--- 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
(
--- 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>
--- 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)
--- 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
--- 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
--- 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
--- 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
--- 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;
--- 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);
--- 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",
--- 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) =
--- 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, _)) =
--- 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"];
--- 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) =
--- 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
--- 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
--- 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
--- 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)
--- 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 *)
--- 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)
--- 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
--- 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
--- 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)
--- 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 =
--- 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;
--- 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
--- 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
--- 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;