# HG changeset patch
# User haftmann
# Date 1256112931 -7200
# Node ID cffdb7b2849864084a9df96fb0b70fe9f328a835
# Parent  5018f6a76b3fbd83b98de6086405182564804707
removed old-style \ and \\ infixes

diff -r 5018f6a76b3f -r cffdb7b28498 src/FOLP/simp.ML
--- 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
diff -r 5018f6a76b3f -r cffdb7b28498 src/HOL/Import/shuffler.ML
--- 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
diff -r 5018f6a76b3f -r cffdb7b28498 src/HOL/Library/normarith.ML
--- 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
diff -r 5018f6a76b3f -r cffdb7b28498 src/HOL/Nominal/nominal_datatype.ML
--- 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
diff -r 5018f6a76b3f -r cffdb7b28498 src/HOL/Nominal/nominal_fresh_fun.ML
--- 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
diff -r 5018f6a76b3f -r cffdb7b28498 src/HOL/Nominal/nominal_inductive.ML
--- 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)
diff -r 5018f6a76b3f -r cffdb7b28498 src/HOL/Nominal/nominal_inductive2.ML
--- 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 =
diff -r 5018f6a76b3f -r cffdb7b28498 src/HOL/Nominal/nominal_primrec.ML
--- 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
diff -r 5018f6a76b3f -r cffdb7b28498 src/HOL/Tools/Datatype/datatype.ML
--- 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) =>
diff -r 5018f6a76b3f -r cffdb7b28498 src/HOL/Tools/Datatype/datatype_case.ML
--- 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" ^
diff -r 5018f6a76b3f -r cffdb7b28498 src/HOL/Tools/Datatype/datatype_rep_proofs.ML
--- 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);
diff -r 5018f6a76b3f -r cffdb7b28498 src/HOL/Tools/Function/fundef_common.ML
--- 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 
diff -r 5018f6a76b3f -r cffdb7b28498 src/HOL/Tools/Function/fundef_lib.ML
--- 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
diff -r 5018f6a76b3f -r cffdb7b28498 src/HOL/Tools/Function/scnp_reconstruct.ML
--- 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
 
 
diff -r 5018f6a76b3f -r cffdb7b28498 src/HOL/Tools/Function/scnp_solve.ML
--- 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 *)
diff -r 5018f6a76b3f -r cffdb7b28498 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- 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')
diff -r 5018f6a76b3f -r cffdb7b28498 src/HOL/Tools/TFL/tfl.ML
--- 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): " ^
diff -r 5018f6a76b3f -r cffdb7b28498 src/HOL/Tools/inductive.ML
--- 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
diff -r 5018f6a76b3f -r cffdb7b28498 src/HOL/Tools/inductive_realizer.ML
--- 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 =
diff -r 5018f6a76b3f -r cffdb7b28498 src/HOL/Tools/old_primrec.ML
--- 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
diff -r 5018f6a76b3f -r cffdb7b28498 src/HOL/Tools/res_axioms.ML
--- 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)
diff -r 5018f6a76b3f -r cffdb7b28498 src/HOL/Tools/res_clause.ML
--- 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;
 
diff -r 5018f6a76b3f -r cffdb7b28498 src/Provers/Arith/cancel_div_mod.ML
--- 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)
diff -r 5018f6a76b3f -r cffdb7b28498 src/Pure/Isar/expression.ML
--- 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 " ^
diff -r 5018f6a76b3f -r cffdb7b28498 src/Pure/library.ML
--- 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 =
diff -r 5018f6a76b3f -r cffdb7b28498 src/Pure/old_goals.ML
--- 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
diff -r 5018f6a76b3f -r cffdb7b28498 src/Tools/atomize_elim.ML
--- 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
diff -r 5018f6a76b3f -r cffdb7b28498 src/ZF/Tools/inductive_package.ML
--- 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