curried inter as canonical list operation (beware of argument order)

--- a/src/HOL/Nominal/nominal_inductive.ML	Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Wed Oct 21 12:09:37 2009 +0200
@@ -28,7 +28,7 @@
 fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
   (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt));
 
-fun preds_of ps t = inter (op = o apfst dest_Free) (ps, Term.add_frees t []);
+fun preds_of ps t = inter (op = o apfst dest_Free) (Term.add_frees t []) ps;
 
 val fresh_prod = thm "fresh_prod";
 

--- a/src/HOL/Nominal/nominal_inductive2.ML	Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Wed Oct 21 12:09:37 2009 +0200
@@ -33,7 +33,7 @@
     [@{thm fresh_star_set_eq}, @{thm fresh_star_Un_elim},
      @{thm fresh_star_insert_elim}, @{thm fresh_star_empty_elim}]);
 
-fun preds_of ps t = inter (op = o apfst dest_Free) (ps, Term.add_frees t []);
+fun preds_of ps t = inter (op = o apfst dest_Free) (Term.add_frees t []) ps;
 
 val perm_bool = mk_meta_eq (thm "perm_bool");
 val perm_boolI = thm "perm_boolI";

--- a/src/HOL/Tools/Function/context_tree.ML	Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/Tools/Function/context_tree.ML	Wed Oct 21 12:09:37 2009 +0200
@@ -90,7 +90,7 @@
       IntGraph.empty
         |> fold (fn (i,_)=> IntGraph.new_node (i,i)) num_branches
         |> fold_product (fn (i, (c1, _)) => fn (j, (_, t2)) => 
-               if i = j orelse null (inter (op =) (c1, t2))
+               if i = j orelse null (inter (op =) c1 t2)
                then I else IntGraph.add_edge_acyclic (i,j))
              num_branches num_branches
     end

--- a/src/HOL/Tools/Function/pattern_split.ML	Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/Tools/Function/pattern_split.ML	Wed Oct 21 12:09:37 2009 +0200
@@ -101,7 +101,7 @@
           let
             val t = Pattern.rewrite_term thy sigma [] feq1
           in
-            fold_rev Logic.all (inter (op =) (map Free (frees_in_term ctx t), vs')) t
+            fold_rev Logic.all (inter (op =) vs' (map Free (frees_in_term ctx t))) t
           end
     in
       map instantiate substs

--- a/src/HOL/Tools/Groebner_Basis/groebner.ML	Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/Tools/Groebner_Basis/groebner.ML	Wed Oct 21 12:09:37 2009 +0200
@@ -884,7 +884,7 @@
  fun isolate_monomials vars tm =
  let 
   val (cmons,vmons) =
-    List.partition (fn m => null (inter op aconvc (frees m, vars)))
+    List.partition (fn m => null (inter (op aconvc) vars (frees m)))
                    (striplist ring_dest_add tm)
   val cofactors = map (fn v => find_multipliers v vmons) vars
   val cnc = if null cmons then zero_tm

--- a/src/HOL/Tools/inductive_codegen.ML	Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Wed Oct 21 12:09:37 2009 +0200
@@ -482,7 +482,7 @@
 fun constrain cs [] = []
   | constrain cs ((s, xs) :: ys) = (s, case AList.lookup (op =) cs (s : string) of
       NONE => xs
-    | SOME xs' => inter (op =) (xs, xs')) :: constrain cs ys;
+    | SOME xs' => inter (op =) xs' xs) :: constrain cs ys;
 
 fun mk_extra_defs thy defs gr dep names module ts =
   Library.foldl (fn (gr, name) =>

--- a/src/HOL/Tools/inductive_set.ML	Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Wed Oct 21 12:09:37 2009 +0200
@@ -209,7 +209,7 @@
       (case optf of
          NONE => fs
        | SOME f => AList.update op = (u, the_default f
-           (Option.map (curry (inter (op =)) f) (AList.lookup op = fs u))) fs));
+           (Option.map (fn g => inter (op =) g f) (AList.lookup op = fs u))) fs));
 
 
 (**************************************************************)

--- a/src/HOL/Tools/record.ML	Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/Tools/record.ML	Wed Oct 21 12:09:37 2009 +0200
@@ -1834,7 +1834,7 @@
     val extN = full bname;
     val types = map snd fields;
     val alphas_fields = fold Term.add_tfree_namesT types [];
-    val alphas_ext = inter (op =) (alphas, alphas_fields);
+    val alphas_ext = inter (op =) alphas_fields alphas;
     val len = length fields;
     val variants =
       Name.variant_list (moreN :: rN :: (rN ^ "'") :: wN :: parent_variants)

--- a/src/HOL/Tools/sat_solver.ML	Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/Tools/sat_solver.ML	Wed Oct 21 12:09:37 2009 +0200
@@ -471,7 +471,7 @@
         | forced_vars False             = []
         | forced_vars (BoolVar i)       = [i]
         | forced_vars (Not (BoolVar i)) = [~i]
-        | forced_vars (Or (fm1, fm2))   = inter (op =) (forced_vars fm1, forced_vars fm2)
+        | forced_vars (Or (fm1, fm2))   = inter (op =) (forced_vars fm1) (forced_vars fm2)
         | forced_vars (And (fm1, fm2))  = union (op =) (forced_vars fm1, forced_vars fm2)
         (* Above, i *and* ~i may be forced.  In this case the first occurrence takes   *)
         (* precedence, and the next partial evaluation of the formula returns 'False'. *)

--- a/src/Provers/Arith/cancel_div_mod.ML	Wed Oct 21 10:15:31 2009 +0200
+++ b/src/Provers/Arith/cancel_div_mod.ML	Wed Oct 21 12:09:37 2009 +0200
@@ -74,7 +74,7 @@
 fun proc ss t =
   let val (divs,mods) = coll_div_mod t ([],[])
   in if null divs orelse null mods then NONE
-     else case inter (op =) (divs, mods) of
+     else case inter (op =) mods divs of
             pq :: _ => SOME (cancel ss t pq)
           | [] => NONE
   end

--- a/src/Pure/General/name_space.ML	Wed Oct 21 10:15:31 2009 +0200
+++ b/src/Pure/General/name_space.ML	Wed Oct 21 12:09:37 2009 +0200
@@ -145,7 +145,7 @@
       space
       |> add_name' name name
       |> fold (del_name name)
-        (if fully then names else inter (op =) (names, [Long_Name.base_name name]))
+        (if fully then names else inter (op =) [Long_Name.base_name name] names)
       |> fold (del_name_extra name) (get_accesses space name)
     end;
 

--- a/src/Pure/General/path.ML	Wed Oct 21 10:15:31 2009 +0200
+++ b/src/Pure/General/path.ML	Wed Oct 21 12:09:37 2009 +0200
@@ -42,7 +42,7 @@
   | check_elem (chs as ["~"]) = err_elem "Illegal" chs
   | check_elem (chs as ["~", "~"]) = err_elem "Illegal" chs
   | check_elem chs =
-      (case inter (op =) (["/", "\\", "$", ":"], chs) of
+      (case inter (op =) ["/", "\\", "$", ":"] chs of
         [] => chs
       | bads => err_elem ("Illegal character(s) " ^ commas_quote bads ^ " in") chs);
 

--- a/src/Pure/library.ML	Wed Oct 21 10:15:31 2009 +0200
+++ b/src/Pure/library.ML	Wed Oct 21 12:09:37 2009 +0200
@@ -158,12 +158,12 @@
   val remove: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list
   val update: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list
   val subtract: ('b * 'a -> bool) -> 'b list -> 'a list -> 'a list
+  val inter: ('a * 'b -> bool) -> 'b list -> 'a list -> 'a list
   val merge: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
   val mem: ''a * ''a list -> bool
   val mem_int: int * int list -> bool
   val mem_string: string * string list -> bool
   val union: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
-  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 distinct: ('a * 'a -> bool) -> 'a list -> 'a list
@@ -782,6 +782,8 @@
 fun remove eq x xs = if member eq xs x then filter_out (fn y => eq (x, y)) xs else xs;
 fun update eq x xs = cons x (remove eq x xs);
 
+fun inter eq xs = filter (member eq xs);
+
 fun subtract eq = fold (remove eq);
 
 fun merge eq (xs, ys) =
@@ -801,12 +803,6 @@
   | union eq ([], ys) = ys
   | union eq (x :: xs, ys) = union eq (xs, insert eq x ys);
 
-(*intersection*)
-fun inter eq ([], ys) = []
-  | inter eq (x::xs, ys) =
-      if member eq ys x then x :: inter eq (xs, ys)
-      else inter eq (xs, ys);
-
 (*subset*)
 fun subset eq (xs, ys) = forall (member eq ys) xs;
 

--- a/src/Pure/pattern.ML	Wed Oct 21 10:15:31 2009 +0200
+++ b/src/Pure/pattern.ML	Wed Oct 21 12:09:37 2009 +0200
@@ -219,7 +219,7 @@
             if subset (op =) (js, is)
             then let val t= mkabs(binders,is,app(Var(G,Gty),map (idx is) js))
                  in Envir.update (((F, Fty), t), env) end
-            else let val ks = inter (op =) (is, js)
+            else let val ks = inter (op =) js is
                      val Hty = type_of_G env (Fty,length is,map (idx is) ks)
                      val (env',H) = Envir.genvar a (env,Hty)
                      fun lam(is) = mkabs(binders,is,app(H,map (idx is) ks));

--- a/src/Pure/thm.ML	Wed Oct 21 10:15:31 2009 +0200
+++ b/src/Pure/thm.ML	Wed Oct 21 12:09:37 2009 +0200
@@ -1463,7 +1463,7 @@
     (case duplicates (op =) cs of
       a :: _ => (warning ("Can't rename.  Bound variables not distinct: " ^ a); state)
     | [] =>
-      (case inter (op =) (cs, freenames) of
+      (case inter (op =) cs freenames of
         a :: _ => (warning ("Can't rename.  Bound/Free variable clash: " ^ a); state)
       | [] =>
         Thm (der,

--- a/src/Pure/variable.ML	Wed Oct 21 10:15:31 2009 +0200
+++ b/src/Pure/variable.ML	Wed Oct 21 12:09:37 2009 +0200
@@ -301,7 +301,7 @@
     val names = names_of ctxt;
     val (xs', names') =
       if is_body ctxt then Name.variants xs names |>> map Name.skolem
-      else (no_dups (inter (op =) (xs, ys)); no_dups (inter (op =) (xs, zs));
+      else (no_dups (inter (op =) xs ys); no_dups (inter (op =) xs zs);
         (xs, fold Name.declare xs names));
   in ctxt |> new_fixes names' xs xs' end;
 

--- a/src/Sequents/prover.ML	Wed Oct 21 10:15:31 2009 +0200
+++ b/src/Sequents/prover.ML	Wed Oct 21 12:09:37 2009 +0200
@@ -31,14 +31,14 @@
        dups);
 
 fun (Pack(safes,unsafes)) add_safes ths   = 
-    let val dups = warn_duplicates (inter Thm.eq_thm_prop (ths,safes))
+    let val dups = warn_duplicates (inter Thm.eq_thm_prop ths safes)
         val ths' = subtract Thm.eq_thm_prop dups ths
     in
         Pack(sort (make_ord less) (ths'@safes), unsafes)
     end;
 
 fun (Pack(safes,unsafes)) add_unsafes ths = 
-    let val dups = warn_duplicates (inter Thm.eq_thm_prop (ths,unsafes))
+    let val dups = warn_duplicates (inter Thm.eq_thm_prop unsafes ths)
         val ths' = subtract Thm.eq_thm_prop dups ths
     in
         Pack(safes, sort (make_ord less) (ths'@unsafes))