# HG changeset patch # User haftmann # Date 1256119941 -7200 # Node ID fe166e8b9f07b39b9973dd0a75e4b84bb5cb67ec # Parent ff71cadefb14894ee2c99297493693a14eabdcfd# Parent c38f02fdf35d7825109c2cc223e4c633ad05a189 merged diff -r ff71cadefb14 -r fe166e8b9f07 src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Wed Oct 21 12:08:52 2009 +0200 +++ b/src/HOL/Nominal/nominal_inductive.ML Wed Oct 21 12:12:21 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"; diff -r ff71cadefb14 -r fe166e8b9f07 src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Wed Oct 21 12:08:52 2009 +0200 +++ b/src/HOL/Nominal/nominal_inductive2.ML Wed Oct 21 12:12:21 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"; diff -r ff71cadefb14 -r fe166e8b9f07 src/HOL/Tools/Function/context_tree.ML --- a/src/HOL/Tools/Function/context_tree.ML Wed Oct 21 12:08:52 2009 +0200 +++ b/src/HOL/Tools/Function/context_tree.ML Wed Oct 21 12:12:21 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 diff -r ff71cadefb14 -r fe166e8b9f07 src/HOL/Tools/Function/pattern_split.ML --- a/src/HOL/Tools/Function/pattern_split.ML Wed Oct 21 12:08:52 2009 +0200 +++ b/src/HOL/Tools/Function/pattern_split.ML Wed Oct 21 12:12:21 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 diff -r ff71cadefb14 -r fe166e8b9f07 src/HOL/Tools/Groebner_Basis/groebner.ML --- a/src/HOL/Tools/Groebner_Basis/groebner.ML Wed Oct 21 12:08:52 2009 +0200 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML Wed Oct 21 12:12:21 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 diff -r ff71cadefb14 -r fe166e8b9f07 src/HOL/Tools/inductive_codegen.ML --- a/src/HOL/Tools/inductive_codegen.ML Wed Oct 21 12:08:52 2009 +0200 +++ b/src/HOL/Tools/inductive_codegen.ML Wed Oct 21 12:12:21 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) => diff -r ff71cadefb14 -r fe166e8b9f07 src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Wed Oct 21 12:08:52 2009 +0200 +++ b/src/HOL/Tools/inductive_set.ML Wed Oct 21 12:12:21 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)); (**************************************************************) diff -r ff71cadefb14 -r fe166e8b9f07 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Wed Oct 21 12:08:52 2009 +0200 +++ b/src/HOL/Tools/record.ML Wed Oct 21 12:12:21 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) diff -r ff71cadefb14 -r fe166e8b9f07 src/HOL/Tools/sat_solver.ML --- a/src/HOL/Tools/sat_solver.ML Wed Oct 21 12:08:52 2009 +0200 +++ b/src/HOL/Tools/sat_solver.ML Wed Oct 21 12:12:21 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'. *) diff -r ff71cadefb14 -r fe166e8b9f07 src/Provers/Arith/cancel_div_mod.ML --- a/src/Provers/Arith/cancel_div_mod.ML Wed Oct 21 12:08:52 2009 +0200 +++ b/src/Provers/Arith/cancel_div_mod.ML Wed Oct 21 12:12:21 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 diff -r ff71cadefb14 -r fe166e8b9f07 src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Wed Oct 21 12:08:52 2009 +0200 +++ b/src/Pure/General/name_space.ML Wed Oct 21 12:12:21 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; diff -r ff71cadefb14 -r fe166e8b9f07 src/Pure/General/path.ML --- a/src/Pure/General/path.ML Wed Oct 21 12:08:52 2009 +0200 +++ b/src/Pure/General/path.ML Wed Oct 21 12:12:21 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); diff -r ff71cadefb14 -r fe166e8b9f07 src/Pure/library.ML --- a/src/Pure/library.ML Wed Oct 21 12:08:52 2009 +0200 +++ b/src/Pure/library.ML Wed Oct 21 12:12:21 2009 +0200 @@ -159,11 +159,11 @@ val update: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list val union: ('a * 'a -> bool) -> 'a list -> '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 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 union eq = fold (insert eq); fun subtract eq = fold (remove eq); @@ -797,16 +799,11 @@ fun (x: int) mem_int xs = member (op =) xs x; fun (x: string) mem_string xs = member (op =) xs x; -(*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*) +(* subset and set equality *) + fun subset eq (xs, ys) = forall (member eq ys) xs; -(*set equality*) fun eq_set eq (xs, ys) = eq_list eq (xs, ys) orelse (subset eq (xs, ys) andalso subset (eq o swap) (ys, xs)); diff -r ff71cadefb14 -r fe166e8b9f07 src/Pure/pattern.ML --- a/src/Pure/pattern.ML Wed Oct 21 12:08:52 2009 +0200 +++ b/src/Pure/pattern.ML Wed Oct 21 12:12:21 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)); diff -r ff71cadefb14 -r fe166e8b9f07 src/Pure/thm.ML --- a/src/Pure/thm.ML Wed Oct 21 12:08:52 2009 +0200 +++ b/src/Pure/thm.ML Wed Oct 21 12:12:21 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, diff -r ff71cadefb14 -r fe166e8b9f07 src/Pure/variable.ML --- a/src/Pure/variable.ML Wed Oct 21 12:08:52 2009 +0200 +++ b/src/Pure/variable.ML Wed Oct 21 12:12:21 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; diff -r ff71cadefb14 -r fe166e8b9f07 src/Sequents/prover.ML --- a/src/Sequents/prover.ML Wed Oct 21 12:08:52 2009 +0200 +++ b/src/Sequents/prover.ML Wed Oct 21 12:12:21 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))