removed old-style \ and \\ infixes
authorhaftmann
Wed Oct 21 10:15:31 2009 +0200 (2009-10-21)
changeset 33040cffdb7b28498
parent 33039 5018f6a76b3f
child 33043 ff71cadefb14
child 33047 69780aef0531
child 33049 c38f02fdf35d
removed old-style \ and \\ infixes
src/FOLP/simp.ML
src/HOL/Import/shuffler.ML
src/HOL/Library/normarith.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_fresh_fun.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Nominal/nominal_primrec.ML
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Datatype/datatype_case.ML
src/HOL/Tools/Datatype/datatype_rep_proofs.ML
src/HOL/Tools/Function/fundef_common.ML
src/HOL/Tools/Function/fundef_lib.ML
src/HOL/Tools/Function/scnp_reconstruct.ML
src/HOL/Tools/Function/scnp_solve.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/TFL/tfl.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/old_primrec.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/res_clause.ML
src/Provers/Arith/cancel_div_mod.ML
src/Pure/Isar/expression.ML
src/Pure/library.ML
src/Pure/old_goals.ML
src/Tools/atomize_elim.ML
src/ZF/Tools/inductive_package.ML
     1.1 --- a/src/FOLP/simp.ML	Wed Oct 21 08:16:25 2009 +0200
     1.2 +++ b/src/FOLP/simp.ML	Wed Oct 21 10:15:31 2009 +0200
     1.3 @@ -543,7 +543,7 @@
     1.4  fun find_subst sg T =
     1.5  let fun find (thm::thms) =
     1.6          let val (Const(_,cT), va, vb) = dest_red(hd(prems_of thm));
     1.7 -            val [P] = OldTerm.add_term_vars(concl_of thm,[]) \\ [va,vb]
     1.8 +            val [P] = subtract (op =) [va, vb] (OldTerm.add_term_vars (concl_of thm, []));
     1.9              val eqT::_ = binder_types cT
    1.10          in if Sign.typ_instance sg (T,eqT) then SOME(thm,va,vb,P)
    1.11             else find thms
     2.1 --- a/src/HOL/Import/shuffler.ML	Wed Oct 21 08:16:25 2009 +0200
     2.2 +++ b/src/HOL/Import/shuffler.ML	Wed Oct 21 10:15:31 2009 +0200
     2.3 @@ -567,15 +567,16 @@
     2.4          end
     2.5      end
     2.6  
     2.7 -val collect_ignored =
     2.8 -    fold_rev (fn thm => fn cs =>
     2.9 -              let
    2.10 -                  val (lhs,rhs) = Logic.dest_equals (prop_of thm)
    2.11 -                  val ignore_lhs = Term.add_const_names lhs [] \\ Term.add_const_names rhs []
    2.12 -                  val ignore_rhs = Term.add_const_names rhs [] \\ Term.add_const_names lhs []
    2.13 -              in
    2.14 -                  fold_rev (insert (op =)) cs (ignore_lhs @ ignore_rhs)
    2.15 -              end)
    2.16 +val collect_ignored = fold_rev (fn thm => fn cs =>
    2.17 +  let
    2.18 +    val (lhs, rhs) = Logic.dest_equals (prop_of thm);
    2.19 +    val consts_lhs = Term.add_const_names lhs [];
    2.20 +    val consts_rhs = Term.add_const_names rhs [];
    2.21 +    val ignore_lhs = subtract (op =) consts_rhs consts_lhs;
    2.22 +    val ignore_rhs = subtract (op =) consts_lhs consts_rhs;
    2.23 +  in
    2.24 +    fold_rev (insert (op =)) cs (ignore_lhs @ ignore_rhs)
    2.25 +  end)
    2.26  
    2.27  (* set_prop t thms tries to make a theorem with the proposition t from
    2.28  one of the theorems thms, by shuffling the propositions around.  If it
     3.1 --- a/src/HOL/Library/normarith.ML	Wed Oct 21 08:16:25 2009 +0200
     3.2 +++ b/src/HOL/Library/normarith.ML	Wed Oct 21 10:15:31 2009 +0200
     3.3 @@ -108,7 +108,7 @@
     3.4           val vdef = int_lincomb_cmul (Rat.neg (Rat.inv c)) eq
     3.5           fun eliminate eqn = if not (FuncUtil.Intfunc.defined eqn v) then eqn 
     3.6                               else int_lincomb_add (int_lincomb_cmul (FuncUtil.Intfunc.apply eqn v) vdef) eqn
     3.7 -        in (case solve (vs \ v,map eliminate oeqs) of
     3.8 +        in (case solve (remove (op =) v vs, map eliminate oeqs) of
     3.9              NONE => NONE
    3.10            | SOME soln => SOME (FuncUtil.Intfunc.update (v, evaluate soln (FuncUtil.Intfunc.delete_safe v vdef)) soln))
    3.11          end
     4.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Wed Oct 21 08:16:25 2009 +0200
     4.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Oct 21 10:15:31 2009 +0200
     4.3 @@ -588,7 +588,7 @@
     4.4      fun mk_perm_closed name = map (fn th => Drule.standard (th RS mp))
     4.5        (List.take (split_conj_thm (Goal.prove_global thy4 [] []
     4.6          (augment_sort thy4
     4.7 -          (pt_class_of thy4 name :: map (cp_class_of thy4 name) (dt_atoms \ name))
     4.8 +          (pt_class_of thy4 name :: map (cp_class_of thy4 name) (remove (op =) name dt_atoms))
     4.9            (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
    4.10              (fn ((s, T), x) =>
    4.11                 let
    4.12 @@ -654,7 +654,7 @@
    4.13            let
    4.14              val pt_class = pt_class_of thy atom;
    4.15              val sort = Sign.certify_sort thy
    4.16 -              (pt_class :: map (cp_class_of thy atom) (dt_atoms \ atom))
    4.17 +              (pt_class :: map (cp_class_of thy atom) (remove (op =) atom dt_atoms))
    4.18            in AxClass.prove_arity
    4.19              (Sign.intern_type thy name,
    4.20                map (inter_sort thy sort o snd) tvs, [pt_class])
    4.21 @@ -678,9 +678,9 @@
    4.22        let
    4.23          val cp_class = cp_class_of thy atom1 atom2;
    4.24          val sort = Sign.certify_sort thy
    4.25 -          (pt_class_of thy atom1 :: map (cp_class_of thy atom1) (dt_atoms \ atom1) @
    4.26 +          (pt_class_of thy atom1 :: map (cp_class_of thy atom1) (remove (op =) atom1 dt_atoms) @
    4.27             (if atom1 = atom2 then [cp_class_of thy atom1 atom1] else
    4.28 -            pt_class_of thy atom2 :: map (cp_class_of thy atom2) (dt_atoms \ atom2)));
    4.29 +            pt_class_of thy atom2 :: map (cp_class_of thy atom2) (remove (op =) atom2 dt_atoms)));
    4.30          val cp1' = cp_inst_of thy atom1 atom2 RS cp1
    4.31        in fold (fn ((((((Abs_inverse, Rep),
    4.32          perm_def), name), tvs), perm_closed1), perm_closed2) => fn thy =>
    4.33 @@ -852,7 +852,7 @@
    4.34        in
    4.35          Goal.prove_global thy8 [] []
    4.36            (augment_sort thy8
    4.37 -            (pt_class_of thy8 atom :: map (cp_class_of thy8 atom) (dt_atoms \ atom))
    4.38 +            (pt_class_of thy8 atom :: map (cp_class_of thy8 atom) (remove (op =) atom dt_atoms))
    4.39              (HOLogic.mk_Trueprop (HOLogic.mk_eq
    4.40                (Const ("Nominal.perm", permT --> U --> U) $ pi $ (Rep $ x),
    4.41                 Rep $ (Const ("Nominal.perm", permT --> T --> T) $ pi $ x)))))
    4.42 @@ -914,7 +914,7 @@
    4.43          in
    4.44            Goal.prove_global thy8 [] []
    4.45              (augment_sort thy8
    4.46 -              (pt_class_of thy8 atom :: map (cp_class_of thy8 atom) (dt_atoms \ atom))
    4.47 +              (pt_class_of thy8 atom :: map (cp_class_of thy8 atom) (remove (op =) atom dt_atoms))
    4.48                (HOLogic.mk_Trueprop (HOLogic.mk_eq
    4.49                  (perm (list_comb (c, l_args)), list_comb (c, r_args)))))
    4.50              (fn _ => EVERY
    4.51 @@ -937,7 +937,7 @@
    4.52  
    4.53      val pt_cp_sort =
    4.54        map (pt_class_of thy8) dt_atoms @
    4.55 -      maps (fn s => map (cp_class_of thy8 s) (dt_atoms \ s)) dt_atoms;
    4.56 +      maps (fn s => map (cp_class_of thy8 s) (remove (op =) s dt_atoms)) dt_atoms;
    4.57  
    4.58      val inject_thms = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) =>
    4.59        let val T = nth_dtyp' i
    4.60 @@ -1276,7 +1276,7 @@
    4.61  
    4.62      val fs_cp_sort =
    4.63        map (fs_class_of thy9) dt_atoms @
    4.64 -      maps (fn s => map (cp_class_of thy9 s) (dt_atoms \ s)) dt_atoms;
    4.65 +      maps (fn s => map (cp_class_of thy9 s) (remove (op =) s dt_atoms)) dt_atoms;
    4.66  
    4.67      (**********************************************************************
    4.68        The subgoals occurring in the proof of induct_aux have the
     5.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Oct 21 08:16:25 2009 +0200
     5.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Oct 21 10:15:31 2009 +0200
     5.3 @@ -151,7 +151,7 @@
     5.4      fun inst_fresh vars params i st =
     5.5     let val vars' = OldTerm.term_vars (prop_of st);
     5.6         val thy = theory_of_thm st;
     5.7 -   in case vars' \\ vars of
     5.8 +   in case subtract (op =) vars vars' of
     5.9       [x] => Seq.single (Thm.instantiate ([],[(cterm_of thy x,cterm_of thy (list_abs (params,Bound 0)))]) st)
    5.10      | _ => error "fresh_fun_simp: Too many variables, please report."
    5.11    end
     6.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Wed Oct 21 08:16:25 2009 +0200
     6.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Wed Oct 21 10:15:31 2009 +0200
     6.3 @@ -154,7 +154,7 @@
     6.4      val elims = map (atomize_induct ctxt) elims;
     6.5      val monos = Inductive.get_monos ctxt;
     6.6      val eqvt_thms = NominalThmDecls.get_eqvt_thms ctxt;
     6.7 -    val _ = (case names \\ fold (Term.add_const_names o Thm.prop_of) eqvt_thms [] of
     6.8 +    val _ = (case subtract (op =) (fold (Term.add_const_names o Thm.prop_of) eqvt_thms []) names of
     6.9          [] => ()
    6.10        | xs => error ("Missing equivariance theorem for predicate(s): " ^
    6.11            commas_quote xs));
    6.12 @@ -170,7 +170,7 @@
    6.13        | xs => error ("Duplicate case names: " ^ commas_quote (map fst xs)));
    6.14      val _ = assert_all (null o duplicates op = o snd) avoids
    6.15        (fn (a, _) => error ("Duplicate variable names for case " ^ quote a));
    6.16 -    val _ = (case map fst avoids \\ induct_cases of
    6.17 +    val _ = (case subtract (op =) induct_cases (map fst avoids) of
    6.18          [] => ()
    6.19        | xs => error ("No such case(s) in inductive definition: " ^ commas_quote xs));
    6.20      val avoids' = if null induct_cases then replicate (length intrs) ("", [])
    6.21 @@ -606,7 +606,7 @@
    6.22          (case duplicates op = atoms of
    6.23               [] => ()
    6.24             | xs => error ("Duplicate atoms: " ^ commas xs);
    6.25 -         case atoms \\ atoms' of
    6.26 +         case subtract (op =) atoms' atoms of
    6.27               [] => ()
    6.28             | xs => error ("No such atoms: " ^ commas xs);
    6.29           atoms)
     7.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Wed Oct 21 08:16:25 2009 +0200
     7.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Wed Oct 21 10:15:31 2009 +0200
     7.3 @@ -160,7 +160,7 @@
     7.4      val elims = map (atomize_induct ctxt) elims;
     7.5      val monos = Inductive.get_monos ctxt;
     7.6      val eqvt_thms = NominalThmDecls.get_eqvt_thms ctxt;
     7.7 -    val _ = (case names \\ fold (Term.add_const_names o Thm.prop_of) eqvt_thms [] of
     7.8 +    val _ = (case subtract (op =) (fold (Term.add_const_names o Thm.prop_of) eqvt_thms []) names of
     7.9          [] => ()
    7.10        | xs => error ("Missing equivariance theorem for predicate(s): " ^
    7.11            commas_quote xs));
    7.12 @@ -176,7 +176,7 @@
    7.13      val _ = (case duplicates (op = o pairself fst) avoids of
    7.14          [] => ()
    7.15        | xs => error ("Duplicate case names: " ^ commas_quote (map fst xs)));
    7.16 -    val _ = (case map fst avoids \\ induct_cases of
    7.17 +    val _ = (case subtract (op =) induct_cases (map fst avoids) of
    7.18          [] => ()
    7.19        | xs => error ("No such case(s) in inductive definition: " ^ commas_quote xs));
    7.20      fun mk_avoids params name sets =
    7.21 @@ -300,7 +300,7 @@
    7.22      val pt_insts = map (NominalAtoms.pt_inst_of thy) atoms;
    7.23      val at_insts = map (NominalAtoms.at_inst_of thy) atoms;
    7.24      val dj_thms = maps (fn a =>
    7.25 -      map (NominalAtoms.dj_thm_of thy a) (atoms \ a)) atoms;
    7.26 +      map (NominalAtoms.dj_thm_of thy a) (remove (op =) a atoms)) atoms;
    7.27      val finite_ineq = map2 (fn th => fn th' => th' RS (th RS
    7.28        @{thm pt_set_finite_ineq})) pt_insts at_insts;
    7.29      val perm_set_forget =
     8.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Wed Oct 21 08:16:25 2009 +0200
     8.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Wed Oct 21 10:15:31 2009 +0200
     8.3 @@ -305,8 +305,8 @@
     8.4        HOLogic.dest_eq |> fst |> strip_comb |> snd |> take_prefix is_Var |> fst;
     8.5      val (pvars, ctxtvars) = List.partition
     8.6        (equal HOLogic.boolT o body_type o snd)
     8.7 -      (fold_rev Term.add_vars (map Logic.strip_assums_concl
     8.8 -        (prems_of (hd rec_rewrites))) [] \\ map dest_Var fvars);
     8.9 +      (subtract (op =) (map dest_Var fvars) (fold_rev Term.add_vars (map Logic.strip_assums_concl
    8.10 +        (prems_of (hd rec_rewrites))) []));
    8.11      val cfs = defs' |> hd |> snd |> strip_comb |> snd |>
    8.12        curry (List.take o swap) (length fvars) |> map cert;
    8.13      val invs' = (case invs of
     9.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Wed Oct 21 08:16:25 2009 +0200
     9.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Wed Oct 21 10:15:31 2009 +0200
     9.3 @@ -504,7 +504,7 @@
     9.4          fun prep_constr (cname, cargs, mx') (constrs, constr_syntax', sorts') =
     9.5            let
     9.6              val (cargs', sorts'') = Library.foldl (prep_typ tmp_thy) (([], sorts'), cargs);
     9.7 -            val _ = (case fold (curry OldTerm.add_typ_tfree_names) cargs' [] \\ tvs of
     9.8 +            val _ = (case subtract (op =) tvs (fold (curry OldTerm.add_typ_tfree_names) cargs' []) of
     9.9                  [] => ()
    9.10                | vs => error ("Extra type variables on rhs: " ^ commas vs))
    9.11            in (constrs @ [(Sign.full_name_path tmp_thy tname'
    9.12 @@ -530,7 +530,7 @@
    9.13  
    9.14      val (dts', constr_syntax, sorts', i) =
    9.15        fold prep_dt_spec (dts ~~ new_type_names) ([], [], [], 0);
    9.16 -    val sorts = sorts' @ (map (rpair (Sign.defaultS tmp_thy)) (tyvars \\ map fst sorts'));
    9.17 +    val sorts = sorts' @ (map (rpair (Sign.defaultS tmp_thy)) (subtract (op =) (map fst sorts') tyvars));
    9.18      val dt_info = get_all thy;
    9.19      val (descr, _) = unfold_datatypes tmp_thy dts' sorts dt_info dts' i;
    9.20      val _ = check_nonempty descr handle (exn as Datatype_Empty s) =>
    10.1 --- a/src/HOL/Tools/Datatype/datatype_case.ML	Wed Oct 21 08:16:25 2009 +0200
    10.2 +++ b/src/HOL/Tools/Datatype/datatype_case.ML	Wed Oct 21 10:15:31 2009 +0200
    10.3 @@ -285,7 +285,7 @@
    10.4      val patts2 = Library.sort (Library.int_ord o Library.pairself row_of_pat) patts1
    10.5      val finals = map row_of_pat patts2
    10.6      val originals = map (row_of_pat o #2) rows
    10.7 -    val _ = case originals \\ finals of
    10.8 +    val _ = case subtract (op =) finals originals of
    10.9          [] => ()
   10.10          | is => (case config of Error => case_error | Warning => warning | Quiet => fn _ => {})
   10.11            ("The following clauses are redundant (covered by preceding clauses):\n" ^
    11.1 --- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Wed Oct 21 08:16:25 2009 +0200
    11.2 +++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Wed Oct 21 10:15:31 2009 +0200
    11.3 @@ -72,8 +72,8 @@
    11.4      val branchTs = get_branching_types descr' sorts;
    11.5      val branchT = if null branchTs then HOLogic.unitT
    11.6        else Balanced_Tree.make (fn (T, U) => Type ("+", [T, U])) branchTs;
    11.7 -    val arities = get_arities descr' \ 0;
    11.8 -    val unneeded_vars = hd tyvars \\ List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs);
    11.9 +    val arities = remove (op =) 0 (get_arities descr');
   11.10 +    val unneeded_vars = subtract (op =) (List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs)) (hd tyvars);
   11.11      val leafTs = leafTs' @ (map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars);
   11.12      val recTs = get_rec_types descr' sorts;
   11.13      val newTs = Library.take (length (hd descr), recTs);
    12.1 --- a/src/HOL/Tools/Function/fundef_common.ML	Wed Oct 21 08:16:25 2009 +0200
    12.2 +++ b/src/HOL/Tools/Function/fundef_common.ML	Wed Oct 21 10:15:31 2009 +0200
    12.3 @@ -234,7 +234,7 @@
    12.4              val _ = length args > 0 orelse input_error "Function has no arguments:"
    12.5  
    12.6              fun add_bvs t is = add_loose_bnos (t, 0, is)
    12.7 -            val rvs = (add_bvs rhs [] \\ fold add_bvs args [])
    12.8 +            val rvs = (subtract (op =) (fold add_bvs args []) (add_bvs rhs []))
    12.9                          |> map (fst o nth (rev qs))
   12.10                        
   12.11              val _ = null rvs orelse input_error 
    13.1 --- a/src/HOL/Tools/Function/fundef_lib.ML	Wed Oct 21 08:16:25 2009 +0200
    13.2 +++ b/src/HOL/Tools/Function/fundef_lib.ML	Wed Oct 21 10:15:31 2009 +0200
    13.3 @@ -153,7 +153,7 @@
    13.4     val mk = HOLogic.mk_binop cn
    13.5     val t = term_of ct
    13.6     val xs = dest_binop_list cn t
    13.7 -   val js = 0 upto (length xs) - 1 \\ is
    13.8 +   val js = subtract (op =) is (0 upto (length xs) - 1)
    13.9     val ty = fastype_of t
   13.10     val thy = theory_of_cterm ct
   13.11   in
    14.1 --- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Wed Oct 21 08:16:25 2009 +0200
    14.2 +++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Wed Oct 21 10:15:31 2009 +0200
    14.3 @@ -240,7 +240,7 @@
    14.4                if is_some (covering g true j) then SOME (j, b) else NONE
    14.5              fun get_wk_cover (j, b) = the (covering g false j)
    14.6  
    14.7 -            val qs = lq \\ map_filter get_str_cover lq
    14.8 +            val qs = subtract (op =) (map_filter get_str_cover lq) lq
    14.9              val ps = map get_wk_cover qs
   14.10  
   14.11              fun indices xs ys = map (fn y => Library.find_index (curry op = y) xs) ys
   14.12 @@ -263,7 +263,8 @@
   14.13              THEN EVERY (map2 (less_proof false) qs ps)
   14.14              THEN (if strict orelse qs <> lq
   14.15                    then LocalDefs.unfold_tac ctxt set_of_simps
   14.16 -                       THEN steps_tac MAX true (lq \\ qs) (lp \\ ps)
   14.17 +                       THEN steps_tac MAX true
   14.18 +                       (subtract (op =) qs lq) (subtract (op =) ps lp)
   14.19                    else all_tac)
   14.20            end
   14.21        in
   14.22 @@ -296,7 +297,7 @@
   14.23             (@{thms split_conv} @ @{thms fst_conv} @ @{thms snd_conv})
   14.24           THEN REPEAT (SOMEGOAL (resolve_tac [@{thm Un_least}, @{thm empty_subsetI}]))
   14.25           THEN EVERY (map (prove_lev true) sl)
   14.26 -         THEN EVERY (map (prove_lev false) ((0 upto length cs - 1) \\ sl)))
   14.27 +         THEN EVERY (map (prove_lev false) (subtract (op =) sl (0 upto length cs - 1))))
   14.28      end
   14.29  
   14.30  
    15.1 --- a/src/HOL/Tools/Function/scnp_solve.ML	Wed Oct 21 08:16:25 2009 +0200
    15.2 +++ b/src/HOL/Tools/Function/scnp_solve.ML	Wed Oct 21 10:15:31 2009 +0200
    15.3 @@ -67,7 +67,7 @@
    15.4  fun iexists n f = PropLogic.exists (map f (0 upto n - 1))
    15.5  fun iforall2 n m f = all (map_product f (0 upto n - 1) (0 upto m - 1))
    15.6  
    15.7 -fun the_one var n x = all (var x :: map (Not o var) ((0 upto n - 1) \\ [x]))
    15.8 +fun the_one var n x = all (var x :: map (Not o var) (remove (op =) x (0 upto n - 1)))
    15.9  fun exactly_one n f = iexists n (the_one f n)
   15.10  
   15.11  (* SAT solving *)
    16.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Oct 21 08:16:25 2009 +0200
    16.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Oct 21 10:15:31 2009 +0200
    16.3 @@ -1051,7 +1051,7 @@
    16.4                    (filter_out (equal p) ps)
    16.5                | _ =>
    16.6                    let 
    16.7 -                    val all_generator_vs = all_subsets (prem_vs \\ vs) |> sort (int_ord o (pairself length))
    16.8 +                    val all_generator_vs = all_subsets (subtract (op =) vs prem_vs) |> sort (int_ord o (pairself length))
    16.9                    in
   16.10                      case (find_first (fn generator_vs => is_some
   16.11                        (select_mode_prem thy modes' (union (op =) (vs, generator_vs)) ps)) all_generator_vs) of
   16.12 @@ -1077,7 +1077,7 @@
   16.13           NONE => NONE
   16.14         | SOME (acc_ps, vs) =>
   16.15           if with_generator then
   16.16 -           SOME (ts, (rev acc_ps) @ (map (generator vTs) (concl_vs \\ vs))) 
   16.17 +           SOME (ts, (rev acc_ps) @ (map (generator vTs) (subtract (op =) vs concl_vs)))
   16.18           else
   16.19             if subset (op =) (concl_vs, vs) then SOME (ts, rev acc_ps) else NONE
   16.20      else NONE
   16.21 @@ -1119,7 +1119,7 @@
   16.22    | remove_from rem ((k, vs) :: xs) =
   16.23      (case AList.lookup (op =) rem k of
   16.24        NONE => (k, vs)
   16.25 -    | SOME vs' => (k, vs \\ vs'))
   16.26 +    | SOME vs' => (k, subtract (op =) vs' vs))
   16.27      :: remove_from rem xs
   16.28      
   16.29  fun infer_modes_with_generator thy extra_modes all_modes param_vs clauses =
   16.30 @@ -2167,7 +2167,7 @@
   16.31                [] => [(i + 1, NONE)]
   16.32              | [U] => [(i + 1, NONE)]
   16.33              | Us =>  (i + 1, NONE) ::
   16.34 -              (map (pair (i + 1) o SOME) ((subsets 1 (length Us)) \\ [[], 1 upto (length Us)])))
   16.35 +              (map (pair (i + 1) o SOME) (subtract (op =) [[], 1 upto (length Us)] (subsets 1 (length Us)))))
   16.36            Ts)
   16.37        in
   16.38          cprod (cprods (map (fn T => case strip_type T of
   16.39 @@ -2218,7 +2218,7 @@
   16.40      val (G', v) = case try (Graph.get_node G) key of
   16.41          SOME v => (G, v)
   16.42        | NONE => (Graph.new_node (key, value_of key) G, value_of key)
   16.43 -    val (G'', visited') = fold (extend' value_of edges_of) (edges_of (key, v) \\ visited)
   16.44 +    val (G'', visited') = fold (extend' value_of edges_of) (subtract (op =) visited (edges_of (key, v)))
   16.45        (G', key :: visited) 
   16.46    in
   16.47      (fold (Graph.add_edge o (pair key)) (edges_of (key, v)) G'', visited')
    17.1 --- a/src/HOL/Tools/TFL/tfl.ML	Wed Oct 21 08:16:25 2009 +0200
    17.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Wed Oct 21 10:15:31 2009 +0200
    17.3 @@ -343,7 +343,7 @@
    17.4       val patts2 = Library.sort (Library.int_ord o Library.pairself row_of_pat) patts1
    17.5       val finals = map row_of_pat patts2
    17.6       val originals = map (row_of_pat o #2) rows
    17.7 -     val dummy = case (originals\\finals)
    17.8 +     val dummy = case (subtract (op =) finals originals)
    17.9               of [] => ()
   17.10            | L => mk_functional_err
   17.11   ("The following clauses are redundant (covered by preceding clauses): " ^
    18.1 --- a/src/HOL/Tools/inductive.ML	Wed Oct 21 08:16:25 2009 +0200
    18.2 +++ b/src/HOL/Tools/inductive.ML	Wed Oct 21 10:15:31 2009 +0200
    18.3 @@ -596,7 +596,7 @@
    18.4      val fp_name = if coind then @{const_name Inductive.gfp} else @{const_name Inductive.lfp};
    18.5  
    18.6      val argTs = fold (fn c => fn Ts => Ts @
    18.7 -      (List.drop (binder_types (fastype_of c), length params) \\ Ts)) cs [];
    18.8 +      (subtract (op =) Ts (List.drop (binder_types (fastype_of c), length params)))) cs [];
    18.9      val k = log 2 1 (length cs);
   18.10      val predT = replicate k HOLogic.boolT ---> argTs ---> HOLogic.boolT;
   18.11      val p :: xs = map Free (Variable.variant_frees ctxt intr_ts
    19.1 --- a/src/HOL/Tools/inductive_realizer.ML	Wed Oct 21 08:16:25 2009 +0200
    19.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Wed Oct 21 10:15:31 2009 +0200
    19.3 @@ -70,7 +70,7 @@
    19.4      val params = map dest_Var (Library.take (nparms, ts));
    19.5      val tname = Binding.name (space_implode "_" (Long_Name.base_name s ^ "T" :: vs));
    19.6      fun constr_of_intr intr = (Binding.name (Long_Name.base_name (name_of_thm intr)),
    19.7 -      map (Logic.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @
    19.8 +      map (Logic.unvarifyT o snd) (subtract (op =) params (rev (Term.add_vars (prop_of intr) []))) @
    19.9          filter_out (equal Extraction.nullT) (map
   19.10            (Logic.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)),
   19.11              NoSyn);
   19.12 @@ -115,7 +115,7 @@
   19.13      val r = if n then Extraction.nullt else Var ((Long_Name.base_name s, 0), rT);
   19.14      val S = list_comb (h, params @ xs);
   19.15      val rvs = relevant_vars S;
   19.16 -    val vs' = map fst rvs \\ vs;
   19.17 +    val vs' = subtract (op =) vs (map fst rvs);
   19.18      val rname = space_implode "_" (s ^ "R" :: vs);
   19.19  
   19.20      fun mk_Tprem n v =
   19.21 @@ -141,7 +141,7 @@
   19.22      val ctxt = ProofContext.init thy
   19.23      val args = map (Free o apfst fst o dest_Var) ivs;
   19.24      val args' = map (Free o apfst fst)
   19.25 -      (Term.add_vars (prop_of intr) [] \\ params);
   19.26 +      (subtract (op =) params (Term.add_vars (prop_of intr) []));
   19.27      val rule' = strip_all rule;
   19.28      val conclT = Extraction.etype_of thy vs [] (Logic.strip_imp_concl rule');
   19.29      val used = map (fst o dest_Free) args;
   19.30 @@ -331,7 +331,7 @@
   19.31      val rintrs = map (fn (intr, c) => Envir.eta_contract
   19.32        (Extraction.realizes_of thy2 vs
   19.33          (if c = Extraction.nullt then c else list_comb (c, map Var (rev
   19.34 -          (Term.add_vars (prop_of intr) []) \\ params'))) (prop_of intr)))
   19.35 +          (subtract (op =) params' (Term.add_vars (prop_of intr) []))))) (prop_of intr)))
   19.36              (maps snd rss ~~ flat constrss);
   19.37      val (rlzpreds, rlzpreds') =
   19.38        rintrs |> map (fn rintr =>
   19.39 @@ -427,9 +427,9 @@
   19.40          val (prem :: prems) = prems_of elim;
   19.41          fun reorder1 (p, (_, intr)) =
   19.42            Library.foldl (fn (t, ((s, _), T)) => Logic.all (Free (s, T)) t)
   19.43 -            (strip_all p, Term.add_vars (prop_of intr) [] \\ params');
   19.44 +            (strip_all p, subtract (op =) params' (Term.add_vars (prop_of intr) []));
   19.45          fun reorder2 ((ivs, intr), i) =
   19.46 -          let val fs = Term.add_vars (prop_of intr) [] \\ params'
   19.47 +          let val fs = subtract (op =) params' (Term.add_vars (prop_of intr) [])
   19.48            in Library.foldl (fn (t, x) => lambda (Var x) t)
   19.49              (list_comb (Bound (i + length ivs), ivs), fs)
   19.50            end;
   19.51 @@ -469,7 +469,7 @@
   19.52      val thy5 = Extraction.add_realizers_i
   19.53        (map (mk_realizer thy4 vs) (map (fn (((rule, rrule), rlz), c) =>
   19.54           (name_of_thm rule, rule, rrule, rlz,
   19.55 -            list_comb (c, map Var (rev (Term.add_vars (prop_of rule) []) \\ params'))))
   19.56 +            list_comb (c, map Var (subtract (op =) params' (rev (Term.add_vars (prop_of rule) []))))))
   19.57                (maps snd rss ~~ #intrs ind_info ~~ rintrs ~~ flat constrss))) thy4;
   19.58      val elimps = map_filter (fn ((s, intrs), p) =>
   19.59        if s mem rsets then SOME (p, intrs) else NONE)
   19.60 @@ -503,7 +503,7 @@
   19.61      add_ind_realizers (hd sets)
   19.62        (case arg of
   19.63          NONE => sets | SOME NONE => []
   19.64 -      | SOME (SOME sets') => sets \\ sets')
   19.65 +      | SOME (SOME sets') => subtract (op =) sets' sets)
   19.66    end I);
   19.67  
   19.68  val setup =
    20.1 --- a/src/HOL/Tools/old_primrec.ML	Wed Oct 21 08:16:25 2009 +0200
    20.2 +++ b/src/HOL/Tools/old_primrec.ML	Wed Oct 21 10:15:31 2009 +0200
    20.3 @@ -90,7 +90,7 @@
    20.4      else
    20.5       (check_vars "repeated variable names in pattern: " (duplicates (op =) lfrees);
    20.6        check_vars "extra variables on rhs: "
    20.7 -        (map dest_Free (OldTerm.term_frees rhs) \\ lfrees);
    20.8 +        (subtract (op =) lfrees (map dest_Free (OldTerm.term_frees rhs)));
    20.9        case AList.lookup (op =) rec_fns fnameT of
   20.10          NONE =>
   20.11            (fnameT, (tname, rpos, [(cname, (ls, cargs, rs, rhs, eq))]))::rec_fns
    21.1 --- a/src/HOL/Tools/res_axioms.ML	Wed Oct 21 08:16:25 2009 +0200
    21.2 +++ b/src/HOL/Tools/res_axioms.ML	Wed Oct 21 10:15:31 2009 +0200
    21.3 @@ -106,7 +106,7 @@
    21.4        fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) defs =
    21.5              (*Existential: declare a Skolem function, then insert into body and continue*)
    21.6              let val skos = map (#1 o Logic.dest_equals) defs  (*existing sko fns*)
    21.7 -                val args = OldTerm.term_frees xtp \\ skos  (*the formal parameters*)
    21.8 +                val args = subtract (op =) skos (OldTerm.term_frees xtp) (*the formal parameters*)
    21.9                  val Ts = map type_of args
   21.10                  val cT = Ts ---> T
   21.11                  val id = "sko_" ^ s ^ "_" ^ Int.toString (Unsynchronized.inc sko_count)
    22.1 --- a/src/HOL/Tools/res_clause.ML	Wed Oct 21 08:16:25 2009 +0200
    22.2 +++ b/src/HOL/Tools/res_clause.ML	Wed Oct 21 10:15:31 2009 +0200
    22.3 @@ -370,7 +370,8 @@
    22.4  fun iter_type_class_pairs thy tycons [] = ([], [])
    22.5    | iter_type_class_pairs thy tycons classes =
    22.6        let val cpairs = type_class_pairs thy tycons classes
    22.7 -          val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs))) \\ classes \\ HOLogic.typeS
    22.8 +          val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs)))
    22.9 +            |> subtract (op =) classes |> subtract (op =) HOLogic.typeS
   22.10            val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
   22.11        in (union (op =) (classes', classes), union (op =) (cpairs', cpairs)) end;
   22.12  
    23.1 --- a/src/Provers/Arith/cancel_div_mod.ML	Wed Oct 21 08:16:25 2009 +0200
    23.2 +++ b/src/Provers/Arith/cancel_div_mod.ML	Wed Oct 21 10:15:31 2009 +0200
    23.3 @@ -65,7 +65,7 @@
    23.4        val d1 = mk_times (snd pq,dpq) and d2 = mk_times (dpq,snd pq)
    23.5        val d = if d1 mem ts then d1 else d2
    23.6        val m = Data.mk_binop Data.mod_name pq
    23.7 -  in mk_plus(mk_plus(d,m),Data.mk_sum(ts \ d \ m)) end
    23.8 +  in mk_plus(mk_plus(d,m),Data.mk_sum(ts |> remove (op =) d |> remove (op =) m)) end
    23.9  
   23.10  fun cancel ss t pq =
   23.11    let val teqt' = Data.prove_eq_sums ss (t, rearrange t pq)
    24.1 --- a/src/Pure/Isar/expression.ML	Wed Oct 21 08:16:25 2009 +0200
    24.2 +++ b/src/Pure/Isar/expression.ML	Wed Oct 21 10:15:31 2009 +0200
    24.3 @@ -628,7 +628,7 @@
    24.4      val xs = filter (member (op =) env o #1) parms;
    24.5      val Ts = map #2 xs;
    24.6      val extraTs =
    24.7 -      (Term.add_tfrees body [] \\ fold Term.add_tfreesT Ts [])
    24.8 +      (subtract (op =) (fold Term.add_tfreesT Ts []) (Term.add_tfrees body []))
    24.9        |> Library.sort_wrt #1 |> map TFree;
   24.10      val predT = map Term.itselfT extraTs ---> Ts ---> bodyT;
   24.11  
   24.12 @@ -738,7 +738,7 @@
   24.13      val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') =
   24.14        define_preds predicate_bname parms text thy;
   24.15  
   24.16 -    val extraTs = fold Term.add_tfrees exts' [] \\ fold Term.add_tfreesT (map snd parms) [];
   24.17 +    val extraTs = subtract (op =) (fold Term.add_tfreesT (map snd parms) []) (fold Term.add_tfrees exts' []);
   24.18      val _ =
   24.19        if null extraTs then ()
   24.20        else warning ("Additional type variable(s) in locale specification " ^
    25.1 --- a/src/Pure/library.ML	Wed Oct 21 08:16:25 2009 +0200
    25.2 +++ b/src/Pure/library.ML	Wed Oct 21 10:15:31 2009 +0200
    25.3 @@ -11,7 +11,7 @@
    25.4  infix 2 ?
    25.5  infix 3 o oo ooo oooo
    25.6  infix 4 ~~ upto downto
    25.7 -infix orf andf \ \\ mem mem_int mem_string
    25.8 +infix orf andf mem mem_int mem_string
    25.9  
   25.10  signature BASIC_LIBRARY =
   25.11  sig
   25.12 @@ -166,8 +166,6 @@
   25.13    val inter: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list
   25.14    val subset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   25.15    val eq_set: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   25.16 -  val \ : ''a list * ''a -> ''a list
   25.17 -  val \\ : ''a list * ''a list -> ''a list
   25.18    val distinct: ('a * 'a -> bool) -> 'a list -> 'a list
   25.19    val duplicates: ('a * 'a -> bool) -> 'a list -> 'a list
   25.20    val has_duplicates: ('a * 'a -> bool) -> 'a list -> bool
   25.21 @@ -818,12 +816,6 @@
   25.22      (subset eq (xs, ys) andalso subset (eq o swap) (ys, xs));
   25.23  
   25.24  
   25.25 -(*removing an element from a list WITHOUT duplicates*)
   25.26 -fun (y :: ys) \ x = if x = y then ys else y :: (ys \ x)
   25.27 -  | [] \ x = [];
   25.28 -fun ys \\ xs = foldl (op \) (ys,xs);
   25.29 -
   25.30 -
   25.31  (*makes a list of the distinct members of the input; preserves order, takes
   25.32    first of equal elements*)
   25.33  fun distinct eq lst =
    26.1 --- a/src/Pure/old_goals.ML	Wed Oct 21 08:16:25 2009 +0200
    26.2 +++ b/src/Pure/old_goals.ML	Wed Oct 21 10:15:31 2009 +0200
    26.3 @@ -259,7 +259,7 @@
    26.4  
    26.5  (*Generates the list of new theories when the proof state's theory changes*)
    26.6  fun thy_error (thy,thy') =
    26.7 -  let val names = Context.display_names thy' \\ Context.display_names thy
    26.8 +  let val names = subtract (op =) (Context.display_names thy) (Context.display_names thy')
    26.9    in  case names of
   26.10          [name] => "\nNew theory: " ^ name
   26.11        | _       => "\nNew theories: " ^ space_implode ", " names
    27.1 --- a/src/Tools/atomize_elim.ML	Wed Oct 21 08:16:25 2009 +0200
    27.2 +++ b/src/Tools/atomize_elim.ML	Wed Oct 21 10:15:31 2009 +0200
    27.3 @@ -34,7 +34,7 @@
    27.4  
    27.5  (* Compute inverse permutation *)
    27.6  fun invert_perm pi =
    27.7 -      (pi @ ((0 upto (fold Integer.max pi 0)) \\ pi))
    27.8 +      (pi @ subtract (op =) pi (0 upto (fold Integer.max pi 0)))
    27.9             |> map_index I
   27.10             |> sort (int_ord o pairself snd)
   27.11             |> map fst
    28.1 --- a/src/ZF/Tools/inductive_package.ML	Wed Oct 21 08:16:25 2009 +0200
    28.2 +++ b/src/ZF/Tools/inductive_package.ML	Wed Oct 21 10:15:31 2009 +0200
    28.3 @@ -110,7 +110,7 @@
    28.4    fun fp_part intr = (*quantify over rule's free vars except parameters*)
    28.5      let val prems = map dest_tprop (Logic.strip_imp_prems intr)
    28.6          val dummy = List.app (fn rec_hd => List.app (chk_prem rec_hd) prems) rec_hds
    28.7 -        val exfrees = OldTerm.term_frees intr \\ rec_params
    28.8 +        val exfrees = subtract (op =) rec_params (OldTerm.term_frees intr)
    28.9          val zeq = FOLogic.mk_eq (Free(z',iT), #1 (rule_concl intr))
   28.10      in List.foldr FOLogic.mk_exists
   28.11               (Balanced_Tree.make FOLogic.mk_conj (zeq::prems)) exfrees
   28.12 @@ -297,7 +297,7 @@
   28.13  
   28.14       (*Make a premise of the induction rule.*)
   28.15       fun induct_prem ind_alist intr =
   28.16 -       let val quantfrees = map dest_Free (OldTerm.term_frees intr \\ rec_params)
   28.17 +       let val quantfrees = map dest_Free (subtract (op =) rec_params (OldTerm.term_frees intr))
   28.18             val iprems = List.foldr (add_induct_prem ind_alist) []
   28.19                                (Logic.strip_imp_prems intr)
   28.20             val (t,X) = Ind_Syntax.rule_concl intr