--- a/src/FOLP/simp.ML Wed Oct 21 08:16:25 2009 +0200
+++ b/src/FOLP/simp.ML Wed Oct 21 10:15:31 2009 +0200
@@ -543,7 +543,7 @@
fun find_subst sg T =
let fun find (thm::thms) =
let val (Const(_,cT), va, vb) = dest_red(hd(prems_of thm));
- val [P] = OldTerm.add_term_vars(concl_of thm,[]) \\ [va,vb]
+ val [P] = subtract (op =) [va, vb] (OldTerm.add_term_vars (concl_of thm, []));
val eqT::_ = binder_types cT
in if Sign.typ_instance sg (T,eqT) then SOME(thm,va,vb,P)
else find thms
--- a/src/HOL/Import/shuffler.ML Wed Oct 21 08:16:25 2009 +0200
+++ b/src/HOL/Import/shuffler.ML Wed Oct 21 10:15:31 2009 +0200
@@ -567,15 +567,16 @@
end
end
-val collect_ignored =
- fold_rev (fn thm => fn cs =>
- let
- val (lhs,rhs) = Logic.dest_equals (prop_of thm)
- val ignore_lhs = Term.add_const_names lhs [] \\ Term.add_const_names rhs []
- val ignore_rhs = Term.add_const_names rhs [] \\ Term.add_const_names lhs []
- in
- fold_rev (insert (op =)) cs (ignore_lhs @ ignore_rhs)
- end)
+val collect_ignored = fold_rev (fn thm => fn cs =>
+ let
+ val (lhs, rhs) = Logic.dest_equals (prop_of thm);
+ val consts_lhs = Term.add_const_names lhs [];
+ val consts_rhs = Term.add_const_names rhs [];
+ val ignore_lhs = subtract (op =) consts_rhs consts_lhs;
+ val ignore_rhs = subtract (op =) consts_lhs consts_rhs;
+ in
+ fold_rev (insert (op =)) cs (ignore_lhs @ ignore_rhs)
+ end)
(* set_prop t thms tries to make a theorem with the proposition t from
one of the theorems thms, by shuffling the propositions around. If it
--- a/src/HOL/Library/normarith.ML Wed Oct 21 08:16:25 2009 +0200
+++ b/src/HOL/Library/normarith.ML Wed Oct 21 10:15:31 2009 +0200
@@ -108,7 +108,7 @@
val vdef = int_lincomb_cmul (Rat.neg (Rat.inv c)) eq
fun eliminate eqn = if not (FuncUtil.Intfunc.defined eqn v) then eqn
else int_lincomb_add (int_lincomb_cmul (FuncUtil.Intfunc.apply eqn v) vdef) eqn
- in (case solve (vs \ v,map eliminate oeqs) of
+ in (case solve (remove (op =) v vs, map eliminate oeqs) of
NONE => NONE
| SOME soln => SOME (FuncUtil.Intfunc.update (v, evaluate soln (FuncUtil.Intfunc.delete_safe v vdef)) soln))
end
--- a/src/HOL/Nominal/nominal_datatype.ML Wed Oct 21 08:16:25 2009 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Wed Oct 21 10:15:31 2009 +0200
@@ -588,7 +588,7 @@
fun mk_perm_closed name = map (fn th => Drule.standard (th RS mp))
(List.take (split_conj_thm (Goal.prove_global thy4 [] []
(augment_sort thy4
- (pt_class_of thy4 name :: map (cp_class_of thy4 name) (dt_atoms \ name))
+ (pt_class_of thy4 name :: map (cp_class_of thy4 name) (remove (op =) name dt_atoms))
(HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
(fn ((s, T), x) =>
let
@@ -654,7 +654,7 @@
let
val pt_class = pt_class_of thy atom;
val sort = Sign.certify_sort thy
- (pt_class :: map (cp_class_of thy atom) (dt_atoms \ atom))
+ (pt_class :: map (cp_class_of thy atom) (remove (op =) atom dt_atoms))
in AxClass.prove_arity
(Sign.intern_type thy name,
map (inter_sort thy sort o snd) tvs, [pt_class])
@@ -678,9 +678,9 @@
let
val cp_class = cp_class_of thy atom1 atom2;
val sort = Sign.certify_sort thy
- (pt_class_of thy atom1 :: map (cp_class_of thy atom1) (dt_atoms \ atom1) @
+ (pt_class_of thy atom1 :: map (cp_class_of thy atom1) (remove (op =) atom1 dt_atoms) @
(if atom1 = atom2 then [cp_class_of thy atom1 atom1] else
- pt_class_of thy atom2 :: map (cp_class_of thy atom2) (dt_atoms \ atom2)));
+ pt_class_of thy atom2 :: map (cp_class_of thy atom2) (remove (op =) atom2 dt_atoms)));
val cp1' = cp_inst_of thy atom1 atom2 RS cp1
in fold (fn ((((((Abs_inverse, Rep),
perm_def), name), tvs), perm_closed1), perm_closed2) => fn thy =>
@@ -852,7 +852,7 @@
in
Goal.prove_global thy8 [] []
(augment_sort thy8
- (pt_class_of thy8 atom :: map (cp_class_of thy8 atom) (dt_atoms \ atom))
+ (pt_class_of thy8 atom :: map (cp_class_of thy8 atom) (remove (op =) atom dt_atoms))
(HOLogic.mk_Trueprop (HOLogic.mk_eq
(Const ("Nominal.perm", permT --> U --> U) $ pi $ (Rep $ x),
Rep $ (Const ("Nominal.perm", permT --> T --> T) $ pi $ x)))))
@@ -914,7 +914,7 @@
in
Goal.prove_global thy8 [] []
(augment_sort thy8
- (pt_class_of thy8 atom :: map (cp_class_of thy8 atom) (dt_atoms \ atom))
+ (pt_class_of thy8 atom :: map (cp_class_of thy8 atom) (remove (op =) atom dt_atoms))
(HOLogic.mk_Trueprop (HOLogic.mk_eq
(perm (list_comb (c, l_args)), list_comb (c, r_args)))))
(fn _ => EVERY
@@ -937,7 +937,7 @@
val pt_cp_sort =
map (pt_class_of thy8) dt_atoms @
- maps (fn s => map (cp_class_of thy8 s) (dt_atoms \ s)) dt_atoms;
+ maps (fn s => map (cp_class_of thy8 s) (remove (op =) s dt_atoms)) dt_atoms;
val inject_thms = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) =>
let val T = nth_dtyp' i
@@ -1276,7 +1276,7 @@
val fs_cp_sort =
map (fs_class_of thy9) dt_atoms @
- maps (fn s => map (cp_class_of thy9 s) (dt_atoms \ s)) dt_atoms;
+ maps (fn s => map (cp_class_of thy9 s) (remove (op =) s dt_atoms)) dt_atoms;
(**********************************************************************
The subgoals occurring in the proof of induct_aux have the
--- a/src/HOL/Nominal/nominal_fresh_fun.ML Wed Oct 21 08:16:25 2009 +0200
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML Wed Oct 21 10:15:31 2009 +0200
@@ -151,7 +151,7 @@
fun inst_fresh vars params i st =
let val vars' = OldTerm.term_vars (prop_of st);
val thy = theory_of_thm st;
- in case vars' \\ vars of
+ in case subtract (op =) vars vars' of
[x] => Seq.single (Thm.instantiate ([],[(cterm_of thy x,cterm_of thy (list_abs (params,Bound 0)))]) st)
| _ => error "fresh_fun_simp: Too many variables, please report."
end
--- a/src/HOL/Nominal/nominal_inductive.ML Wed Oct 21 08:16:25 2009 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Wed Oct 21 10:15:31 2009 +0200
@@ -154,7 +154,7 @@
val elims = map (atomize_induct ctxt) elims;
val monos = Inductive.get_monos ctxt;
val eqvt_thms = NominalThmDecls.get_eqvt_thms ctxt;
- val _ = (case names \\ fold (Term.add_const_names o Thm.prop_of) eqvt_thms [] of
+ val _ = (case subtract (op =) (fold (Term.add_const_names o Thm.prop_of) eqvt_thms []) names of
[] => ()
| xs => error ("Missing equivariance theorem for predicate(s): " ^
commas_quote xs));
@@ -170,7 +170,7 @@
| xs => error ("Duplicate case names: " ^ commas_quote (map fst xs)));
val _ = assert_all (null o duplicates op = o snd) avoids
(fn (a, _) => error ("Duplicate variable names for case " ^ quote a));
- val _ = (case map fst avoids \\ induct_cases of
+ val _ = (case subtract (op =) induct_cases (map fst avoids) of
[] => ()
| xs => error ("No such case(s) in inductive definition: " ^ commas_quote xs));
val avoids' = if null induct_cases then replicate (length intrs) ("", [])
@@ -606,7 +606,7 @@
(case duplicates op = atoms of
[] => ()
| xs => error ("Duplicate atoms: " ^ commas xs);
- case atoms \\ atoms' of
+ case subtract (op =) atoms' atoms of
[] => ()
| xs => error ("No such atoms: " ^ commas xs);
atoms)
--- a/src/HOL/Nominal/nominal_inductive2.ML Wed Oct 21 08:16:25 2009 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Wed Oct 21 10:15:31 2009 +0200
@@ -160,7 +160,7 @@
val elims = map (atomize_induct ctxt) elims;
val monos = Inductive.get_monos ctxt;
val eqvt_thms = NominalThmDecls.get_eqvt_thms ctxt;
- val _ = (case names \\ fold (Term.add_const_names o Thm.prop_of) eqvt_thms [] of
+ val _ = (case subtract (op =) (fold (Term.add_const_names o Thm.prop_of) eqvt_thms []) names of
[] => ()
| xs => error ("Missing equivariance theorem for predicate(s): " ^
commas_quote xs));
@@ -176,7 +176,7 @@
val _ = (case duplicates (op = o pairself fst) avoids of
[] => ()
| xs => error ("Duplicate case names: " ^ commas_quote (map fst xs)));
- val _ = (case map fst avoids \\ induct_cases of
+ val _ = (case subtract (op =) induct_cases (map fst avoids) of
[] => ()
| xs => error ("No such case(s) in inductive definition: " ^ commas_quote xs));
fun mk_avoids params name sets =
@@ -300,7 +300,7 @@
val pt_insts = map (NominalAtoms.pt_inst_of thy) atoms;
val at_insts = map (NominalAtoms.at_inst_of thy) atoms;
val dj_thms = maps (fn a =>
- map (NominalAtoms.dj_thm_of thy a) (atoms \ a)) atoms;
+ map (NominalAtoms.dj_thm_of thy a) (remove (op =) a atoms)) atoms;
val finite_ineq = map2 (fn th => fn th' => th' RS (th RS
@{thm pt_set_finite_ineq})) pt_insts at_insts;
val perm_set_forget =
--- a/src/HOL/Nominal/nominal_primrec.ML Wed Oct 21 08:16:25 2009 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML Wed Oct 21 10:15:31 2009 +0200
@@ -305,8 +305,8 @@
HOLogic.dest_eq |> fst |> strip_comb |> snd |> take_prefix is_Var |> fst;
val (pvars, ctxtvars) = List.partition
(equal HOLogic.boolT o body_type o snd)
- (fold_rev Term.add_vars (map Logic.strip_assums_concl
- (prems_of (hd rec_rewrites))) [] \\ map dest_Var fvars);
+ (subtract (op =) (map dest_Var fvars) (fold_rev Term.add_vars (map Logic.strip_assums_concl
+ (prems_of (hd rec_rewrites))) []));
val cfs = defs' |> hd |> snd |> strip_comb |> snd |>
curry (List.take o swap) (length fvars) |> map cert;
val invs' = (case invs of
--- a/src/HOL/Tools/Datatype/datatype.ML Wed Oct 21 08:16:25 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML Wed Oct 21 10:15:31 2009 +0200
@@ -504,7 +504,7 @@
fun prep_constr (cname, cargs, mx') (constrs, constr_syntax', sorts') =
let
val (cargs', sorts'') = Library.foldl (prep_typ tmp_thy) (([], sorts'), cargs);
- val _ = (case fold (curry OldTerm.add_typ_tfree_names) cargs' [] \\ tvs of
+ val _ = (case subtract (op =) tvs (fold (curry OldTerm.add_typ_tfree_names) cargs' []) of
[] => ()
| vs => error ("Extra type variables on rhs: " ^ commas vs))
in (constrs @ [(Sign.full_name_path tmp_thy tname'
@@ -530,7 +530,7 @@
val (dts', constr_syntax, sorts', i) =
fold prep_dt_spec (dts ~~ new_type_names) ([], [], [], 0);
- val sorts = sorts' @ (map (rpair (Sign.defaultS tmp_thy)) (tyvars \\ map fst sorts'));
+ val sorts = sorts' @ (map (rpair (Sign.defaultS tmp_thy)) (subtract (op =) (map fst sorts') tyvars));
val dt_info = get_all thy;
val (descr, _) = unfold_datatypes tmp_thy dts' sorts dt_info dts' i;
val _ = check_nonempty descr handle (exn as Datatype_Empty s) =>
--- a/src/HOL/Tools/Datatype/datatype_case.ML Wed Oct 21 08:16:25 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_case.ML Wed Oct 21 10:15:31 2009 +0200
@@ -285,7 +285,7 @@
val patts2 = Library.sort (Library.int_ord o Library.pairself row_of_pat) patts1
val finals = map row_of_pat patts2
val originals = map (row_of_pat o #2) rows
- val _ = case originals \\ finals of
+ val _ = case subtract (op =) finals originals of
[] => ()
| is => (case config of Error => case_error | Warning => warning | Quiet => fn _ => {})
("The following clauses are redundant (covered by preceding clauses):\n" ^
--- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Wed Oct 21 08:16:25 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Wed Oct 21 10:15:31 2009 +0200
@@ -72,8 +72,8 @@
val branchTs = get_branching_types descr' sorts;
val branchT = if null branchTs then HOLogic.unitT
else Balanced_Tree.make (fn (T, U) => Type ("+", [T, U])) branchTs;
- val arities = get_arities descr' \ 0;
- val unneeded_vars = hd tyvars \\ List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs);
+ val arities = remove (op =) 0 (get_arities descr');
+ val unneeded_vars = subtract (op =) (List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs)) (hd tyvars);
val leafTs = leafTs' @ (map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars);
val recTs = get_rec_types descr' sorts;
val newTs = Library.take (length (hd descr), recTs);
--- a/src/HOL/Tools/Function/fundef_common.ML Wed Oct 21 08:16:25 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_common.ML Wed Oct 21 10:15:31 2009 +0200
@@ -234,7 +234,7 @@
val _ = length args > 0 orelse input_error "Function has no arguments:"
fun add_bvs t is = add_loose_bnos (t, 0, is)
- val rvs = (add_bvs rhs [] \\ fold add_bvs args [])
+ val rvs = (subtract (op =) (fold add_bvs args []) (add_bvs rhs []))
|> map (fst o nth (rev qs))
val _ = null rvs orelse input_error
--- a/src/HOL/Tools/Function/fundef_lib.ML Wed Oct 21 08:16:25 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_lib.ML Wed Oct 21 10:15:31 2009 +0200
@@ -153,7 +153,7 @@
val mk = HOLogic.mk_binop cn
val t = term_of ct
val xs = dest_binop_list cn t
- val js = 0 upto (length xs) - 1 \\ is
+ val js = subtract (op =) is (0 upto (length xs) - 1)
val ty = fastype_of t
val thy = theory_of_cterm ct
in
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML Wed Oct 21 08:16:25 2009 +0200
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Wed Oct 21 10:15:31 2009 +0200
@@ -240,7 +240,7 @@
if is_some (covering g true j) then SOME (j, b) else NONE
fun get_wk_cover (j, b) = the (covering g false j)
- val qs = lq \\ map_filter get_str_cover lq
+ val qs = subtract (op =) (map_filter get_str_cover lq) lq
val ps = map get_wk_cover qs
fun indices xs ys = map (fn y => Library.find_index (curry op = y) xs) ys
@@ -263,7 +263,8 @@
THEN EVERY (map2 (less_proof false) qs ps)
THEN (if strict orelse qs <> lq
then LocalDefs.unfold_tac ctxt set_of_simps
- THEN steps_tac MAX true (lq \\ qs) (lp \\ ps)
+ THEN steps_tac MAX true
+ (subtract (op =) qs lq) (subtract (op =) ps lp)
else all_tac)
end
in
@@ -296,7 +297,7 @@
(@{thms split_conv} @ @{thms fst_conv} @ @{thms snd_conv})
THEN REPEAT (SOMEGOAL (resolve_tac [@{thm Un_least}, @{thm empty_subsetI}]))
THEN EVERY (map (prove_lev true) sl)
- THEN EVERY (map (prove_lev false) ((0 upto length cs - 1) \\ sl)))
+ THEN EVERY (map (prove_lev false) (subtract (op =) sl (0 upto length cs - 1))))
end
--- a/src/HOL/Tools/Function/scnp_solve.ML Wed Oct 21 08:16:25 2009 +0200
+++ b/src/HOL/Tools/Function/scnp_solve.ML Wed Oct 21 10:15:31 2009 +0200
@@ -67,7 +67,7 @@
fun iexists n f = PropLogic.exists (map f (0 upto n - 1))
fun iforall2 n m f = all (map_product f (0 upto n - 1) (0 upto m - 1))
-fun the_one var n x = all (var x :: map (Not o var) ((0 upto n - 1) \\ [x]))
+fun the_one var n x = all (var x :: map (Not o var) (remove (op =) x (0 upto n - 1)))
fun exactly_one n f = iexists n (the_one f n)
(* SAT solving *)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Oct 21 08:16:25 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Oct 21 10:15:31 2009 +0200
@@ -1051,7 +1051,7 @@
(filter_out (equal p) ps)
| _ =>
let
- val all_generator_vs = all_subsets (prem_vs \\ vs) |> sort (int_ord o (pairself length))
+ val all_generator_vs = all_subsets (subtract (op =) vs prem_vs) |> sort (int_ord o (pairself length))
in
case (find_first (fn generator_vs => is_some
(select_mode_prem thy modes' (union (op =) (vs, generator_vs)) ps)) all_generator_vs) of
@@ -1077,7 +1077,7 @@
NONE => NONE
| SOME (acc_ps, vs) =>
if with_generator then
- SOME (ts, (rev acc_ps) @ (map (generator vTs) (concl_vs \\ vs)))
+ SOME (ts, (rev acc_ps) @ (map (generator vTs) (subtract (op =) vs concl_vs)))
else
if subset (op =) (concl_vs, vs) then SOME (ts, rev acc_ps) else NONE
else NONE
@@ -1119,7 +1119,7 @@
| remove_from rem ((k, vs) :: xs) =
(case AList.lookup (op =) rem k of
NONE => (k, vs)
- | SOME vs' => (k, vs \\ vs'))
+ | SOME vs' => (k, subtract (op =) vs' vs))
:: remove_from rem xs
fun infer_modes_with_generator thy extra_modes all_modes param_vs clauses =
@@ -2167,7 +2167,7 @@
[] => [(i + 1, NONE)]
| [U] => [(i + 1, NONE)]
| Us => (i + 1, NONE) ::
- (map (pair (i + 1) o SOME) ((subsets 1 (length Us)) \\ [[], 1 upto (length Us)])))
+ (map (pair (i + 1) o SOME) (subtract (op =) [[], 1 upto (length Us)] (subsets 1 (length Us)))))
Ts)
in
cprod (cprods (map (fn T => case strip_type T of
@@ -2218,7 +2218,7 @@
val (G', v) = case try (Graph.get_node G) key of
SOME v => (G, v)
| NONE => (Graph.new_node (key, value_of key) G, value_of key)
- val (G'', visited') = fold (extend' value_of edges_of) (edges_of (key, v) \\ visited)
+ val (G'', visited') = fold (extend' value_of edges_of) (subtract (op =) visited (edges_of (key, v)))
(G', key :: visited)
in
(fold (Graph.add_edge o (pair key)) (edges_of (key, v)) G'', visited')
--- a/src/HOL/Tools/TFL/tfl.ML Wed Oct 21 08:16:25 2009 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML Wed Oct 21 10:15:31 2009 +0200
@@ -343,7 +343,7 @@
val patts2 = Library.sort (Library.int_ord o Library.pairself row_of_pat) patts1
val finals = map row_of_pat patts2
val originals = map (row_of_pat o #2) rows
- val dummy = case (originals\\finals)
+ val dummy = case (subtract (op =) finals originals)
of [] => ()
| L => mk_functional_err
("The following clauses are redundant (covered by preceding clauses): " ^
--- a/src/HOL/Tools/inductive.ML Wed Oct 21 08:16:25 2009 +0200
+++ b/src/HOL/Tools/inductive.ML Wed Oct 21 10:15:31 2009 +0200
@@ -596,7 +596,7 @@
val fp_name = if coind then @{const_name Inductive.gfp} else @{const_name Inductive.lfp};
val argTs = fold (fn c => fn Ts => Ts @
- (List.drop (binder_types (fastype_of c), length params) \\ Ts)) cs [];
+ (subtract (op =) Ts (List.drop (binder_types (fastype_of c), length params)))) cs [];
val k = log 2 1 (length cs);
val predT = replicate k HOLogic.boolT ---> argTs ---> HOLogic.boolT;
val p :: xs = map Free (Variable.variant_frees ctxt intr_ts
--- a/src/HOL/Tools/inductive_realizer.ML Wed Oct 21 08:16:25 2009 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Wed Oct 21 10:15:31 2009 +0200
@@ -70,7 +70,7 @@
val params = map dest_Var (Library.take (nparms, ts));
val tname = Binding.name (space_implode "_" (Long_Name.base_name s ^ "T" :: vs));
fun constr_of_intr intr = (Binding.name (Long_Name.base_name (name_of_thm intr)),
- map (Logic.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @
+ map (Logic.unvarifyT o snd) (subtract (op =) params (rev (Term.add_vars (prop_of intr) []))) @
filter_out (equal Extraction.nullT) (map
(Logic.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)),
NoSyn);
@@ -115,7 +115,7 @@
val r = if n then Extraction.nullt else Var ((Long_Name.base_name s, 0), rT);
val S = list_comb (h, params @ xs);
val rvs = relevant_vars S;
- val vs' = map fst rvs \\ vs;
+ val vs' = subtract (op =) vs (map fst rvs);
val rname = space_implode "_" (s ^ "R" :: vs);
fun mk_Tprem n v =
@@ -141,7 +141,7 @@
val ctxt = ProofContext.init thy
val args = map (Free o apfst fst o dest_Var) ivs;
val args' = map (Free o apfst fst)
- (Term.add_vars (prop_of intr) [] \\ params);
+ (subtract (op =) params (Term.add_vars (prop_of intr) []));
val rule' = strip_all rule;
val conclT = Extraction.etype_of thy vs [] (Logic.strip_imp_concl rule');
val used = map (fst o dest_Free) args;
@@ -331,7 +331,7 @@
val rintrs = map (fn (intr, c) => Envir.eta_contract
(Extraction.realizes_of thy2 vs
(if c = Extraction.nullt then c else list_comb (c, map Var (rev
- (Term.add_vars (prop_of intr) []) \\ params'))) (prop_of intr)))
+ (subtract (op =) params' (Term.add_vars (prop_of intr) []))))) (prop_of intr)))
(maps snd rss ~~ flat constrss);
val (rlzpreds, rlzpreds') =
rintrs |> map (fn rintr =>
@@ -427,9 +427,9 @@
val (prem :: prems) = prems_of elim;
fun reorder1 (p, (_, intr)) =
Library.foldl (fn (t, ((s, _), T)) => Logic.all (Free (s, T)) t)
- (strip_all p, Term.add_vars (prop_of intr) [] \\ params');
+ (strip_all p, subtract (op =) params' (Term.add_vars (prop_of intr) []));
fun reorder2 ((ivs, intr), i) =
- let val fs = Term.add_vars (prop_of intr) [] \\ params'
+ let val fs = subtract (op =) params' (Term.add_vars (prop_of intr) [])
in Library.foldl (fn (t, x) => lambda (Var x) t)
(list_comb (Bound (i + length ivs), ivs), fs)
end;
@@ -469,7 +469,7 @@
val thy5 = Extraction.add_realizers_i
(map (mk_realizer thy4 vs) (map (fn (((rule, rrule), rlz), c) =>
(name_of_thm rule, rule, rrule, rlz,
- list_comb (c, map Var (rev (Term.add_vars (prop_of rule) []) \\ params'))))
+ list_comb (c, map Var (subtract (op =) params' (rev (Term.add_vars (prop_of rule) []))))))
(maps snd rss ~~ #intrs ind_info ~~ rintrs ~~ flat constrss))) thy4;
val elimps = map_filter (fn ((s, intrs), p) =>
if s mem rsets then SOME (p, intrs) else NONE)
@@ -503,7 +503,7 @@
add_ind_realizers (hd sets)
(case arg of
NONE => sets | SOME NONE => []
- | SOME (SOME sets') => sets \\ sets')
+ | SOME (SOME sets') => subtract (op =) sets' sets)
end I);
val setup =
--- a/src/HOL/Tools/old_primrec.ML Wed Oct 21 08:16:25 2009 +0200
+++ b/src/HOL/Tools/old_primrec.ML Wed Oct 21 10:15:31 2009 +0200
@@ -90,7 +90,7 @@
else
(check_vars "repeated variable names in pattern: " (duplicates (op =) lfrees);
check_vars "extra variables on rhs: "
- (map dest_Free (OldTerm.term_frees rhs) \\ lfrees);
+ (subtract (op =) lfrees (map dest_Free (OldTerm.term_frees rhs)));
case AList.lookup (op =) rec_fns fnameT of
NONE =>
(fnameT, (tname, rpos, [(cname, (ls, cargs, rs, rhs, eq))]))::rec_fns
--- a/src/HOL/Tools/res_axioms.ML Wed Oct 21 08:16:25 2009 +0200
+++ b/src/HOL/Tools/res_axioms.ML Wed Oct 21 10:15:31 2009 +0200
@@ -106,7 +106,7 @@
fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) defs =
(*Existential: declare a Skolem function, then insert into body and continue*)
let val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*)
- val args = OldTerm.term_frees xtp \\ skos (*the formal parameters*)
+ val args = subtract (op =) skos (OldTerm.term_frees xtp) (*the formal parameters*)
val Ts = map type_of args
val cT = Ts ---> T
val id = "sko_" ^ s ^ "_" ^ Int.toString (Unsynchronized.inc sko_count)
--- a/src/HOL/Tools/res_clause.ML Wed Oct 21 08:16:25 2009 +0200
+++ b/src/HOL/Tools/res_clause.ML Wed Oct 21 10:15:31 2009 +0200
@@ -370,7 +370,8 @@
fun iter_type_class_pairs thy tycons [] = ([], [])
| iter_type_class_pairs thy tycons classes =
let val cpairs = type_class_pairs thy tycons classes
- val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs))) \\ classes \\ HOLogic.typeS
+ val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs)))
+ |> subtract (op =) classes |> subtract (op =) HOLogic.typeS
val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
in (union (op =) (classes', classes), union (op =) (cpairs', cpairs)) end;
--- a/src/Provers/Arith/cancel_div_mod.ML Wed Oct 21 08:16:25 2009 +0200
+++ b/src/Provers/Arith/cancel_div_mod.ML Wed Oct 21 10:15:31 2009 +0200
@@ -65,7 +65,7 @@
val d1 = mk_times (snd pq,dpq) and d2 = mk_times (dpq,snd pq)
val d = if d1 mem ts then d1 else d2
val m = Data.mk_binop Data.mod_name pq
- in mk_plus(mk_plus(d,m),Data.mk_sum(ts \ d \ m)) end
+ in mk_plus(mk_plus(d,m),Data.mk_sum(ts |> remove (op =) d |> remove (op =) m)) end
fun cancel ss t pq =
let val teqt' = Data.prove_eq_sums ss (t, rearrange t pq)
--- a/src/Pure/Isar/expression.ML Wed Oct 21 08:16:25 2009 +0200
+++ b/src/Pure/Isar/expression.ML Wed Oct 21 10:15:31 2009 +0200
@@ -628,7 +628,7 @@
val xs = filter (member (op =) env o #1) parms;
val Ts = map #2 xs;
val extraTs =
- (Term.add_tfrees body [] \\ fold Term.add_tfreesT Ts [])
+ (subtract (op =) (fold Term.add_tfreesT Ts []) (Term.add_tfrees body []))
|> Library.sort_wrt #1 |> map TFree;
val predT = map Term.itselfT extraTs ---> Ts ---> bodyT;
@@ -738,7 +738,7 @@
val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') =
define_preds predicate_bname parms text thy;
- val extraTs = fold Term.add_tfrees exts' [] \\ fold Term.add_tfreesT (map snd parms) [];
+ val extraTs = subtract (op =) (fold Term.add_tfreesT (map snd parms) []) (fold Term.add_tfrees exts' []);
val _ =
if null extraTs then ()
else warning ("Additional type variable(s) in locale specification " ^
--- a/src/Pure/library.ML Wed Oct 21 08:16:25 2009 +0200
+++ b/src/Pure/library.ML Wed Oct 21 10:15:31 2009 +0200
@@ -11,7 +11,7 @@
infix 2 ?
infix 3 o oo ooo oooo
infix 4 ~~ upto downto
-infix orf andf \ \\ mem mem_int mem_string
+infix orf andf mem mem_int mem_string
signature BASIC_LIBRARY =
sig
@@ -166,8 +166,6 @@
val inter: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list
val subset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
val eq_set: ('a * 'b -> bool) -> 'a list * 'b list -> bool
- val \ : ''a list * ''a -> ''a list
- val \\ : ''a list * ''a list -> ''a list
val distinct: ('a * 'a -> bool) -> 'a list -> 'a list
val duplicates: ('a * 'a -> bool) -> 'a list -> 'a list
val has_duplicates: ('a * 'a -> bool) -> 'a list -> bool
@@ -818,12 +816,6 @@
(subset eq (xs, ys) andalso subset (eq o swap) (ys, xs));
-(*removing an element from a list WITHOUT duplicates*)
-fun (y :: ys) \ x = if x = y then ys else y :: (ys \ x)
- | [] \ x = [];
-fun ys \\ xs = foldl (op \) (ys,xs);
-
-
(*makes a list of the distinct members of the input; preserves order, takes
first of equal elements*)
fun distinct eq lst =
--- a/src/Pure/old_goals.ML Wed Oct 21 08:16:25 2009 +0200
+++ b/src/Pure/old_goals.ML Wed Oct 21 10:15:31 2009 +0200
@@ -259,7 +259,7 @@
(*Generates the list of new theories when the proof state's theory changes*)
fun thy_error (thy,thy') =
- let val names = Context.display_names thy' \\ Context.display_names thy
+ let val names = subtract (op =) (Context.display_names thy) (Context.display_names thy')
in case names of
[name] => "\nNew theory: " ^ name
| _ => "\nNew theories: " ^ space_implode ", " names
--- a/src/Tools/atomize_elim.ML Wed Oct 21 08:16:25 2009 +0200
+++ b/src/Tools/atomize_elim.ML Wed Oct 21 10:15:31 2009 +0200
@@ -34,7 +34,7 @@
(* Compute inverse permutation *)
fun invert_perm pi =
- (pi @ ((0 upto (fold Integer.max pi 0)) \\ pi))
+ (pi @ subtract (op =) pi (0 upto (fold Integer.max pi 0)))
|> map_index I
|> sort (int_ord o pairself snd)
|> map fst
--- a/src/ZF/Tools/inductive_package.ML Wed Oct 21 08:16:25 2009 +0200
+++ b/src/ZF/Tools/inductive_package.ML Wed Oct 21 10:15:31 2009 +0200
@@ -110,7 +110,7 @@
fun fp_part intr = (*quantify over rule's free vars except parameters*)
let val prems = map dest_tprop (Logic.strip_imp_prems intr)
val dummy = List.app (fn rec_hd => List.app (chk_prem rec_hd) prems) rec_hds
- val exfrees = OldTerm.term_frees intr \\ rec_params
+ val exfrees = subtract (op =) rec_params (OldTerm.term_frees intr)
val zeq = FOLogic.mk_eq (Free(z',iT), #1 (rule_concl intr))
in List.foldr FOLogic.mk_exists
(Balanced_Tree.make FOLogic.mk_conj (zeq::prems)) exfrees
@@ -297,7 +297,7 @@
(*Make a premise of the induction rule.*)
fun induct_prem ind_alist intr =
- let val quantfrees = map dest_Free (OldTerm.term_frees intr \\ rec_params)
+ let val quantfrees = map dest_Free (subtract (op =) rec_params (OldTerm.term_frees intr))
val iprems = List.foldr (add_induct_prem ind_alist) []
(Logic.strip_imp_prems intr)
val (t,X) = Ind_Syntax.rule_concl intr