--- a/src/HOL/Import/hol4rews.ML Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/Import/hol4rews.ML Wed Oct 21 12:08:52 2009 +0200
@@ -165,7 +165,7 @@
val empty = []
val copy = I
val extend = I
- fun merge _ = Library.union Thm.eq_thm
+ fun merge _ = Library.merge Thm.eq_thm_prop
)
val hol4_debug = Unsynchronized.ref false
--- a/src/HOL/Import/shuffler.ML Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/Import/shuffler.ML Wed Oct 21 12:08:52 2009 +0200
@@ -78,7 +78,7 @@
val empty = []
val copy = I
val extend = I
- fun merge _ = Library.union Thm.eq_thm
+ fun merge _ = Library.merge Thm.eq_thm_prop
)
fun print_shuffles thy =
--- a/src/HOL/Library/Sum_Of_Squares.thy Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/Library/Sum_Of_Squares.thy Wed Oct 21 12:08:52 2009 +0200
@@ -9,10 +9,10 @@
theory Sum_Of_Squares
imports Complex_Main (* "~~/src/HOL/Decision_Procs/Dense_Linear_Order" *)
uses
- ("positivstellensatz.ML") (* duplicate use!? -- cf. Euclidian_Space.thy *)
- ("Sum_Of_Squares/sum_of_squares.ML")
- ("Sum_Of_Squares/positivstellensatz_tools.ML")
- ("Sum_Of_Squares/sos_wrapper.ML")
+ "positivstellensatz.ML" (* duplicate use!? -- cf. Euclidian_Space.thy *)
+ "Sum_Of_Squares/sum_of_squares.ML"
+ "Sum_Of_Squares/positivstellensatz_tools.ML"
+ "Sum_Of_Squares/sos_wrapper.ML"
begin
text {*
@@ -28,13 +28,6 @@
without calling an external prover.
*}
-text {* setup sos tactic *}
-
-use "positivstellensatz.ML"
-use "Sum_Of_Squares/positivstellensatz_tools.ML"
-use "Sum_Of_Squares/sum_of_squares.ML"
-use "Sum_Of_Squares/sos_wrapper.ML"
-
setup SOS_Wrapper.setup
text {* Tests *}
--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Wed Oct 21 12:08:52 2009 +0200
@@ -244,7 +244,7 @@
fun monomial_lcm m1 m2 =
fold_rev (fn x => FuncUtil.Ctermfunc.update (x, max (monomial_degree x m1) (monomial_degree x m2)))
- (union (is_equal o FuncUtil.cterm_ord) (FuncUtil.Ctermfunc.dom m1, FuncUtil.Ctermfunc.dom m2)) (FuncUtil.Ctermfunc.empty);
+ (union (is_equal o FuncUtil.cterm_ord) (FuncUtil.Ctermfunc.dom m1) (FuncUtil.Ctermfunc.dom m2)) (FuncUtil.Ctermfunc.empty);
fun monomial_multidegree m =
FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => k + a) m 0;;
@@ -314,7 +314,7 @@
FuncUtil.Monomialfunc.fold (fn (m, c) => fn a => max (monomial_multidegree m) a) p 0;
fun poly_variables p =
- sort FuncUtil.cterm_ord (FuncUtil.Monomialfunc.fold_rev (fn (m, c) => curry (union (is_equal o FuncUtil.cterm_ord)) (monomial_variables m)) p []);;
+ sort FuncUtil.cterm_ord (FuncUtil.Monomialfunc.fold_rev (fn (m, c) => union (is_equal o FuncUtil.cterm_ord) (monomial_variables m)) p []);;
(* Order monomials for human presentation. *)
@@ -1059,8 +1059,8 @@
fun real_positivnullstellensatz_general prover linf d eqs leqs pol =
let
- val vars = fold_rev (curry (union (op aconvc)) o poly_variables)
- (pol::eqs @ map fst leqs) []
+ val vars = fold_rev (union (op aconvc) o poly_variables)
+ (pol :: eqs @ map fst leqs) []
val monoid = if linf then
(poly_const rat_1,RealArith.Rational_lt rat_1)::
(filter (fn (p,c) => multidegree p <= d) leqs)
--- a/src/HOL/Library/normarith.ML Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/Library/normarith.ML Wed Oct 21 12:08:52 2009 +0200
@@ -286,7 +286,7 @@
val dests = distinct (op aconvc) (map snd rawdests)
val srcfuns = map vector_lincomb sources
val destfuns = map vector_lincomb dests
- val vvs = fold_rev (curry (union op aconvc) o FuncUtil.Ctermfunc.dom) (srcfuns @ destfuns) []
+ val vvs = fold_rev (union (op aconvc) o FuncUtil.Ctermfunc.dom) (srcfuns @ destfuns) []
val n = length srcfuns
val nvs = 1 upto n
val srccombs = srcfuns ~~ nvs
--- a/src/HOL/Library/positivstellensatz.ML Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/Library/positivstellensatz.ML Wed Oct 21 12:08:52 2009 +0200
@@ -620,7 +620,7 @@
| NONE => (case eqs of
[] =>
let val vars = remove (op aconvc) one_tm
- (fold_rev (curry (union (op aconvc)) o FuncUtil.Ctermfunc.dom o fst) (les@lts) [])
+ (fold_rev (union (op aconvc) o FuncUtil.Ctermfunc.dom o fst) (les@lts) [])
in linear_ineqs vars (les,lts) end
| (e,p)::es =>
if FuncUtil.Ctermfunc.is_empty e then linear_eqs (es,les,lts) else
@@ -679,7 +679,7 @@
val le_pols = map rhs le
val lt_pols = map rhs lt
val aliens = filter is_alien
- (fold_rev (curry (union (op aconvc)) o FuncUtil.Ctermfunc.dom)
+ (fold_rev (union (op aconvc) o FuncUtil.Ctermfunc.dom)
(eq_pols @ le_pols @ lt_pols) [])
val le_pols' = le_pols @ map (fn v => FuncUtil.Ctermfunc.onefunc (v,Rat.one)) aliens
val (_,proof) = linear_prover (eq_pols,le_pols',lt_pols)
--- a/src/HOL/SEQ.thy Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/SEQ.thy Wed Oct 21 12:08:52 2009 +0200
@@ -1089,10 +1089,10 @@
subsubsection {* Cauchy Sequences are Convergent *}
-axclass complete_space \<subseteq> metric_space
- Cauchy_convergent: "Cauchy X \<Longrightarrow> convergent X"
+class complete_space =
+ assumes Cauchy_convergent: "Cauchy X \<Longrightarrow> convergent X"
-axclass banach \<subseteq> real_normed_vector, complete_space
+class banach = real_normed_vector + complete_space
theorem LIMSEQ_imp_Cauchy:
assumes X: "X ----> a" shows "Cauchy X"
--- a/src/HOL/Tools/Datatype/datatype_aux.ML Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML Wed Oct 21 12:08:52 2009 +0200
@@ -257,7 +257,7 @@
fun get_nonrec_types descr sorts =
map (typ_of_dtyp descr sorts) (Library.foldl (fn (Ts, (_, (_, _, constrs))) =>
Library.foldl (fn (Ts', (_, cargs)) =>
- union (op =) (filter_out is_rec_type cargs, Ts')) (Ts, constrs)) ([], descr));
+ union (op =) (filter_out is_rec_type cargs) Ts') (Ts, constrs)) ([], descr));
(* get all recursive types in datatype description *)
--- 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:08:52 2009 +0200
@@ -348,7 +348,7 @@
| Add(lin1,lin2) =>
let val lis1 = resolve_proof vars lin1
val lis2 = resolve_proof vars lin2
- val dom = distinct (op =) (union (op =) (map fst lis1, map fst lis2))
+ val dom = distinct (op =) (union (op =) (map fst lis1) (map fst lis2))
in
map (fn n => let val a = these (AList.lookup (op =) lis1 n)
val b = these (AList.lookup (op =) lis2 n)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Oct 21 12:08:52 2009 +0200
@@ -1047,16 +1047,16 @@
(if with_generator then
(case select_mode_prem thy gen_modes' vs ps of
SOME (p as Prem _, SOME mode) => check_mode_prems ((gen_prem p, mode) :: acc_ps)
- (case p of Prem (us, _) => union (op =) (vs, terms_vs us) | _ => vs)
+ (case p of Prem (us, _) => union (op =) vs (terms_vs us) | _ => vs)
(filter_out (equal p) ps)
| _ =>
let
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
+ (select_mode_prem thy modes' (union (op =) vs generator_vs) ps)) all_generator_vs) of
SOME generator_vs => check_mode_prems ((map (generator vTs) generator_vs) @ acc_ps)
- (union (op =) (vs, generator_vs)) ps
+ (union (op =) vs generator_vs) ps
| NONE => let
val _ = tracing ("ps:" ^ (commas
(map (fn p => string_of_moded_prem thy (p, Mode (([], []), [], []))) ps)))
@@ -1065,7 +1065,7 @@
else
NONE)
| SOME (p, SOME mode) => check_mode_prems ((if with_generator then param_gen_prem param_vs p else p, mode) :: acc_ps)
- (case p of Prem (us, _) => union (op =) (vs, terms_vs us) | _ => vs)
+ (case p of Prem (us, _) => union (op =) vs (terms_vs us) | _ => vs)
(filter_out (equal p) ps))
val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (split_smode is ts));
val in_vs = terms_vs in_ts;
@@ -1073,7 +1073,7 @@
in
if forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso
forall (is_eqT o fastype_of) in_ts' then
- case check_mode_prems [] (union (op =) (param_vs, in_vs)) ps of
+ case check_mode_prems [] (union (op =) param_vs in_vs) ps of
NONE => NONE
| SOME (acc_ps, vs) =>
if with_generator then
--- a/src/HOL/Tools/Qelim/cooper.ML Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Wed Oct 21 12:08:52 2009 +0200
@@ -308,7 +308,7 @@
| Const (@{const_name Not},_)$_ => h (acc,dacc) (Thm.dest_arg t)
| _ => (acc, dacc)
val (cs,ds) = h ([],[]) p
- val l = Integer.lcms (union (op =) (cs, ds))
+ val l = Integer.lcms (union (op =) cs ds)
fun cv k ct =
let val (tm as b$s$t) = term_of ct
in ((HOLogic.eq_const bT)$tm$(b$(linear_cmul k s)$(linear_cmul k t))
--- a/src/HOL/Tools/TFL/post.ML Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/Tools/TFL/post.ML Wed Oct 21 12:08:52 2009 +0200
@@ -28,7 +28,7 @@
*--------------------------------------------------------------------------*)
fun termination_goals rules =
map (Type.freeze o HOLogic.dest_Trueprop)
- (List.foldr (fn (th,A) => union (op aconv) (prems_of th, A)) [] rules);
+ (List.foldr (fn (th,A) => uncurry (union (op aconv)) (prems_of th, A)) [] rules);
(*---------------------------------------------------------------------------
* Three postprocessors are applied to the definition. It
@@ -79,7 +79,7 @@
val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th)))
val cntxtl = (#1 o S.strip_imp) lhs (* cntxtl should = cntxtr *)
val cntxtr = (#1 o S.strip_imp) rhs (* but union is solider *)
- val cntxt = union (op aconv) (cntxtl, cntxtr)
+ val cntxt = union (op aconv) cntxtl cntxtr
in
R.GEN_ALL
(R.DISCH_ALL
--- a/src/HOL/Tools/TFL/tfl.ML Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML Wed Oct 21 12:08:52 2009 +0200
@@ -531,7 +531,7 @@
then writeln (cat_lines ("Extractants =" ::
map (Display.string_of_thm_global thy) extractants))
else ()
- val TCs = List.foldr (union (op aconv)) [] TCl
+ val TCs = List.foldr (uncurry (union (op aconv))) [] TCl
val full_rqt = WFR::TCs
val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt}
val R'abs = S.rand R'
--- 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:08:52 2009 +0200
@@ -222,7 +222,7 @@
| check_mode_prems vs ps = (case select_mode_prem thy modes' vs ps of
NONE => NONE
| SOME (x, _) => check_mode_prems
- (case x of Prem (us, _, _) => union (op =) (vs, terms_vs us) | _ => vs)
+ (case x of Prem (us, _, _) => union (op =) vs (terms_vs us) | _ => vs)
(filter_out (equal x) ps));
val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (get_args is 1 ts));
val in_vs = terms_vs in_ts;
@@ -230,7 +230,7 @@
in
forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso
forall (is_eqT o fastype_of) in_ts' andalso
- (case check_mode_prems (union (op =) (arg_vs, in_vs)) ps of
+ (case check_mode_prems (union (op =) arg_vs in_vs) ps of
NONE => false
| SOME vs => subset (op =) (concl_vs, vs))
end;
--- a/src/HOL/Tools/metis_tools.ML Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/Tools/metis_tools.ML Wed Oct 21 12:08:52 2009 +0200
@@ -631,7 +631,7 @@
let val (mth, tfree_lits) = hol_thm_to_fol is_conjecture ctxt mode ith
in
{axioms = (mth, Meson.make_meta_clause ith) :: axioms,
- tfrees = union (op =) (tfree_lits, tfrees)}
+ tfrees = union (op =) tfree_lits tfrees}
end;
val lmap0 = List.foldl (add_thm true)
{axioms = [], tfrees = init_tfrees ctxt} cls
--- a/src/HOL/Tools/prop_logic.ML Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/Tools/prop_logic.ML Wed Oct 21 12:08:52 2009 +0200
@@ -111,8 +111,8 @@
| indices False = []
| indices (BoolVar i) = [i]
| indices (Not fm) = indices fm
- | indices (Or (fm1, fm2)) = union (op =) (indices fm1, indices fm2)
- | indices (And (fm1, fm2)) = union (op =) (indices fm1, indices fm2);
+ | indices (Or (fm1, fm2)) = union (op =) (indices fm1) (indices fm2)
+ | indices (And (fm1, fm2)) = union (op =) (indices fm1) (indices fm2);
(* ------------------------------------------------------------------------- *)
(* maxidx: computes the maximal variable index occuring in a formula of *)
--- a/src/HOL/Tools/refute.ML Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/Tools/refute.ML Wed Oct 21 12:08:52 2009 +0200
@@ -1154,7 +1154,7 @@
val axioms = collect_axioms thy u
(* Term.typ list *)
val types = Library.foldl (fn (acc, t') =>
- union (op =) (acc, (ground_types thy t'))) ([], u :: axioms)
+ uncurry (union (op =)) (acc, (ground_types thy t'))) ([], u :: axioms)
val _ = tracing ("Ground types: "
^ (if null types then "none."
else commas (map (Syntax.string_of_typ_global thy) types)))
--- a/src/HOL/Tools/res_axioms.ML Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/Tools/res_axioms.ML Wed Oct 21 12:08:52 2009 +0200
@@ -473,7 +473,7 @@
val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs))
(map Thm.term_of hyps)
val fixed = OldTerm.term_frees (concl_of st) @
- List.foldl (union (op aconv)) [] (map OldTerm.term_frees remaining_hyps)
+ List.foldl (uncurry (union (op aconv))) [] (map OldTerm.term_frees remaining_hyps)
in Seq.of_list [LocalDefs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end;
--- a/src/HOL/Tools/res_clause.ML Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/Tools/res_clause.ML Wed Oct 21 12:08:52 2009 +0200
@@ -93,7 +93,7 @@
val tconst_prefix = "tc_";
val class_prefix = "class_";
-fun union_all xss = List.foldl (union (op =)) [] xss;
+fun union_all xss = List.foldl (uncurry (union (op =))) [] xss;
(*Provide readable names for the more common symbolic functions*)
val const_trans_table =
@@ -263,7 +263,7 @@
| pred_of_sort (LTFree (s,ty)) = (s,1)
(*Given a list of sorted type variables, return a list of type literals.*)
-fun add_typs Ts = List.foldl (union (op =)) [] (map sorts_on_typs Ts);
+fun add_typs Ts = List.foldl (uncurry (union (op =))) [] (map sorts_on_typs Ts);
(*The correct treatment of TFrees like 'a in lemmas (axiom clauses) is not clear.
* Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a
@@ -373,7 +373,7 @@
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;
+ in (union (op =) classes' classes, union (op =) cpairs' cpairs) end;
fun make_arity_clauses_dfg dfg thy tycons classes =
let val (classes', cpairs) = iter_type_class_pairs thy tycons classes
--- a/src/HOL/Tools/res_hol_clause.ML Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/Tools/res_hol_clause.ML Wed Oct 21 12:08:52 2009 +0200
@@ -155,7 +155,7 @@
| combterm_of dfg thy (P $ Q) =
let val (P',tsP) = combterm_of dfg thy P
val (Q',tsQ) = combterm_of dfg thy Q
- in (CombApp(P',Q'), union (op =) (tsP, tsQ)) end
+ in (CombApp(P',Q'), union (op =) tsP tsQ) end
| combterm_of _ _ (t as Abs _) = raise RC.CLAUSE ("HOL CLAUSE", t);
fun predicate_of dfg thy ((Const("Not",_) $ P), polarity) = predicate_of dfg thy (P, not polarity)
@@ -167,7 +167,7 @@
| literals_of_term1 dfg thy (lits,ts) P =
let val ((pred,ts'),pol) = predicate_of dfg thy (P,true)
in
- (Literal(pol,pred)::lits, union (op =) (ts, ts'))
+ (Literal(pol,pred)::lits, union (op =) ts ts')
end;
fun literals_of_term_dfg dfg thy P = literals_of_term1 dfg thy ([],[]) P;
@@ -476,7 +476,7 @@
val (cma, cnh) = count_constants clauses
val params = (t_full, cma, cnh)
val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures)
- val tfree_clss = map RC.tptp_tfree_clause (List.foldl (union (op =)) [] tfree_litss)
+ val tfree_clss = map RC.tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss)
val _ =
File.write_list file (
map (#1 o (clause2tptp params)) axclauses @
--- a/src/HOL/Tools/res_reconstruct.ML Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML Wed Oct 21 12:08:52 2009 +0200
@@ -364,7 +364,7 @@
fun replace_dep (old:int, new) dep = if dep=old then new else [dep];
fun replace_deps (old:int, new) (lno, t, deps) =
- (lno, t, List.foldl (union (op =)) [] (map (replace_dep (old, new)) deps));
+ (lno, t, List.foldl (uncurry (union (op =))) [] (map (replace_dep (old, new)) deps));
(*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ
only in type information.*)
--- 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:08:52 2009 +0200
@@ -472,7 +472,7 @@
| 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 (And (fm1, fm2)) = union (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'. *)
| forced_vars _ = error "formula is not in negation normal form"
--- a/src/HOL/Tools/transfer.ML Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/Tools/transfer.ML Wed Oct 21 12:08:52 2009 +0200
@@ -143,7 +143,7 @@
{inj = h inj0 inj1 inj2, emb = h emb0 emb1 emb2,
ret = h ret0 ret1 ret2, cong = h cg0 cg1 cg2, guess = g1 andalso g2,
hints = subtract (op = : string*string -> bool) hints0
- (union (op =) (hints1, hints2))}
+ (union (op =) hints1 hints2)}
end;
local
@@ -151,7 +151,7 @@
in
fun merge_entries ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1},
{inj = inj2, emb = emb2, ret = ret2, cong = cg2, guess = g2, hints = hints2}) =
- {inj = h inj1 inj2, emb = h emb1 emb2, ret = h ret1 ret2, cong = h cg1 cg2, guess = g1 andalso g2, hints = union (op =) (hints1, hints2)}
+ {inj = h inj1 inj2, emb = h emb1 emb2, ret = h ret1 ret2, cong = h cg1 cg2, guess = g1 andalso g2, hints = union (op =) hints1 hints2}
end;
fun add ((inja,injd), (emba,embd), (reta,retd), (cga,cgd), g, (hintsa, hintsd)) =
--- a/src/HOL/ex/Codegenerator_Candidates.thy Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/ex/Codegenerator_Candidates.thy Wed Oct 21 12:08:52 2009 +0200
@@ -26,7 +26,7 @@
"~~/src/HOL/ex/Records"
begin
-(*avoid popular infixes*)
-code_reserved SML union inter upto
+(*avoid popular infix*)
+code_reserved SML upto
end
--- a/src/HOL/ex/predicate_compile.ML Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML Wed Oct 21 12:08:52 2009 +0200
@@ -964,22 +964,22 @@
(if with_generator then
(case select_mode_prem thy gen_modes' vs ps of
SOME (p, SOME mode) => check_mode_prems ((gen_prem p, mode) :: acc_ps)
- (case p of Prem (us, _) => union (op =) (vs, terms_vs us) | _ => vs)
+ (case p of Prem (us, _) => union (op =) vs (terms_vs us) | _ => vs)
(filter_out (equal p) ps)
| NONE =>
let
val all_generator_vs = all_subsets (prem_vs \\ 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
+ (select_mode_prem thy modes' (union (op =) vs generator_vs) ps)) all_generator_vs) of
SOME generator_vs => check_mode_prems ((map (generator vTs) generator_vs) @ acc_ps)
- (union (op =) (vs, generator_vs)) ps
+ (union (op =) vs generator_vs) ps
| NONE => NONE
end)
else
NONE)
| SOME (p, SOME mode) => check_mode_prems ((if with_generator then param_gen_prem param_vs p else p, mode) :: acc_ps)
- (case p of Prem (us, _) => union (op =) (vs, terms_vs us) | _ => vs)
+ (case p of Prem (us, _) => union (op =) vs (terms_vs us) | _ => vs)
(filter_out (equal p) ps))
val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (split_smode is ts));
val in_vs = terms_vs in_ts;
@@ -987,7 +987,7 @@
in
if forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso
forall (is_eqT o fastype_of) in_ts' then
- case check_mode_prems [] (union (op =) (param_vs, in_vs)) ps of
+ case check_mode_prems [] (union (op =) param_vs in_vs) ps of
NONE => NONE
| SOME (acc_ps, vs) =>
if with_generator then
--- a/src/Provers/Arith/fast_lin_arith.ML Wed Oct 21 10:15:31 2009 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Wed Oct 21 12:08:52 2009 +0200
@@ -385,7 +385,7 @@
let val (eqs, noneqs) = List.partition (fn (Lineq(_,ty,_,_)) => ty=Eq) nontriv in
if not (null eqs) then
let val c =
- fold (fn Lineq(_,_,l,_) => fn cs => union (op =) (l, cs)) eqs []
+ fold (fn Lineq(_,_,l,_) => fn cs => union (op =) l cs) eqs []
|> filter (fn i => i <> 0)
|> sort (int_ord o pairself abs)
|> hd
@@ -429,9 +429,8 @@
val warning_count = Unsynchronized.ref 0;
val warning_count_max = 10;
-val union_term = curry (union Pattern.aeconv);
-val union_bterm = curry (union
- (fn ((b:bool, t), (b', t')) => b = b' andalso Pattern.aeconv (t, t')));
+val union_term = union Pattern.aeconv;
+val union_bterm = union (fn ((b:bool, t), (b', t')) => b = b' andalso Pattern.aeconv (t, t'));
fun add_atoms (lhs, _, _, rhs, _, _) =
union_term (map fst lhs) o union_term (map fst rhs);
--- a/src/Pure/Proof/reconstruct.ML Wed Oct 21 10:15:31 2009 +0200
+++ b/src/Pure/Proof/reconstruct.ML Wed Oct 21 12:08:52 2009 +0200
@@ -289,7 +289,7 @@
val _ = message "Collecting constraints...";
val (t, prf, cs, env, _) = make_constraints_cprf thy
(Envir.empty (maxidx_proof cprf ~1)) cprf';
- val cs' = map (fn p => (true, p, union (op =)
+ val cs' = map (fn p => (true, p, uncurry (union (op =))
(pairself (map (fst o dest_Var) o OldTerm.term_vars) p)))
(map (pairself (Envir.norm_term env)) ((t, prop')::cs));
val _ = message ("Solving remaining constraints (" ^ string_of_int (length cs') ^ ") ...");
--- a/src/Pure/Syntax/parser.ML Wed Oct 21 10:15:31 2009 +0200
+++ b/src/Pure/Syntax/parser.ML Wed Oct 21 12:08:52 2009 +0200
@@ -101,7 +101,7 @@
val tos = connected_with chains' [lhs] [lhs];
in (copy_lookahead tos [],
- union (op =) (if member (op =) lambdas lhs then tos else [], lambdas))
+ union (op =) (if member (op =) lambdas lhs then tos else []) lambdas)
end;
(*test if new production can produce lambda
@@ -109,7 +109,7 @@
val (new_lambda, lambdas') =
if forall (fn (Nonterminal (id, _)) => member (op =) lambdas' id
| (Terminal _) => false) rhs then
- (true, union (op =) (lambdas', connected_with chains' [lhs] [lhs]))
+ (true, union (op =) lambdas' (connected_with chains' [lhs] [lhs]))
else
(false, lambdas');
@@ -125,7 +125,7 @@
(*get all known starting tokens for a nonterminal*)
fun starts_for_nt nt = snd (fst (Array.sub (prods, nt)));
- val token_union = union matching_tokens;
+ val token_union = uncurry (union matching_tokens);
(*update prods, lookaheads, and lambdas according to new lambda NTs*)
val (added_starts', lambdas') =
@@ -155,7 +155,7 @@
val added_tks' = token_union (new_tks, added_tks);
- val nt_dependencies' = union (op =) (nts, nt_dependencies);
+ val nt_dependencies' = union (op =) nts nt_dependencies;
(*associate production with new starting tokens*)
fun copy ([]: token option list) nt_prods = nt_prods
@@ -413,7 +413,7 @@
fun prod_of_chain from = ([Nonterminal (from, ~1)], "", ~1);
val nt_prods =
- Library.foldl (union op =) ([], map snd (snd (Array.sub (prods, tag)))) @
+ Library.foldl (uncurry (union (op =))) ([], map snd (snd (Array.sub (prods, tag)))) @
map prod_of_chain ((these o AList.lookup (op =) chains) tag);
in map (pretty_prod name) nt_prods end;
@@ -562,8 +562,8 @@
fun process_nt ~1 result = result
| process_nt nt result =
let
- val nt_prods = Library.foldl (union op =)
- ([], map snd (snd (Array.sub (prods2, nt))));
+ val nt_prods = Library.foldl (uncurry (union (op =)))
+ ([], map snd (snd (Array.sub (prods2, nt))));
val lhs_tag = convert_tag nt;
(*convert tags in rhs*)
--- a/src/Pure/Syntax/syn_ext.ML Wed Oct 21 10:15:31 2009 +0200
+++ b/src/Pure/Syntax/syn_ext.ML Wed Oct 21 12:08:52 2009 +0200
@@ -352,7 +352,7 @@
in
SynExt {
xprods = xprods,
- consts = union (op =) (consts, mfix_consts),
+ consts = union (op =) consts mfix_consts,
prmodes = distinct (op =) (map (fn (m, _, _) => m) tokentrfuns),
parse_ast_translation = parse_ast_translation,
parse_rules = parse_rules' @ parse_rules,
--- a/src/Pure/codegen.ML Wed Oct 21 10:15:31 2009 +0200
+++ b/src/Pure/codegen.ML Wed Oct 21 12:08:52 2009 +0200
@@ -599,8 +599,8 @@
else Pretty.block (separate (Pretty.brk 1) (p :: ps));
fun new_names t xs = Name.variant_list
- (union (op =) (map (fst o fst o dest_Var) (OldTerm.term_vars t),
- OldTerm.add_term_names (t, ML_Syntax.reserved_names))) (map mk_id xs);
+ (union (op =) (map (fst o fst o dest_Var) (OldTerm.term_vars t))
+ (OldTerm.add_term_names (t, ML_Syntax.reserved_names))) (map mk_id xs);
fun new_name t x = hd (new_names t [x]);
--- a/src/Pure/library.ML Wed Oct 21 10:15:31 2009 +0200
+++ b/src/Pure/library.ML Wed Oct 21 12:08:52 2009 +0200
@@ -157,12 +157,12 @@
val insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list
val remove: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list
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 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
@@ -782,6 +782,7 @@
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 union eq = fold (insert eq);
fun subtract eq = fold (remove eq);
fun merge eq (xs, ys) =
@@ -796,11 +797,6 @@
fun (x: int) mem_int xs = member (op =) xs x;
fun (x: string) mem_string xs = member (op =) xs x;
-(*union of sets represented as lists: no repetitions*)
-fun union eq (xs, []) = xs
- | 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) =
--- a/src/Pure/proofterm.ML Wed Oct 21 10:15:31 2009 +0200
+++ b/src/Pure/proofterm.ML Wed Oct 21 12:08:52 2009 +0200
@@ -900,7 +900,7 @@
fun add_funvars Ts (vs, t) =
if is_fun (fastype_of1 (Ts, t)) then
- union (op =) (vs, map_filter (fn Var (ixn, T) =>
+ union (op =) vs (map_filter (fn Var (ixn, T) =>
if is_fun T then SOME ixn else NONE | _ => NONE) (vars_of t))
else vs;
@@ -918,7 +918,7 @@
| (Abs (_, T, u), ts) => Library.foldl (add_npvars' (T::Ts)) (vs, u :: ts)
| (_, ts) => Library.foldl (add_npvars' Ts) (vs, ts));
-fun prop_vars (Const ("==>", _) $ P $ Q) = union (op =) (prop_vars P, prop_vars Q)
+fun prop_vars (Const ("==>", _) $ P $ Q) = union (op =) (prop_vars P) (prop_vars Q)
| prop_vars (Const ("all", _) $ Abs (_, _, t)) = prop_vars t
| prop_vars t = (case strip_comb t of
(Var (ixn, _), _) => [ixn] | _ => []);
@@ -936,9 +936,9 @@
end;
fun needed_vars prop =
- union (op =) (Library.foldl (union (op =))
- ([], map (uncurry (insert (op =))) (add_npvars true true [] ([], prop))),
- prop_vars prop);
+ union (op =) (Library.foldl (uncurry (union (op =)))
+ ([], map (uncurry (insert (op =))) (add_npvars true true [] ([], prop))))
+ (prop_vars prop);
fun gen_axm_proof c name prop =
let
@@ -975,7 +975,7 @@
let
val p as (_, is', ch', prf') = shrink ls lev prf2;
val (is, ch, ts', prf'') = shrink' ls lev ts (p::prfs) prf1
- in (union (op =) (is, is'), ch orelse ch', ts',
+ in (union (op =) is is', ch orelse ch', ts',
if ch orelse ch' then prf'' %% prf' else prf)
end
| shrink' ls lev ts prfs (prf as prf1 % t) =
@@ -1004,15 +1004,15 @@
val insts = Library.take (length ts', map (fst o dest_Var) vs) ~~ ts';
val nvs = Library.foldl (fn (ixns', (ixn, ixns)) =>
insert (op =) ixn (case AList.lookup (op =) insts ixn of
- SOME (SOME t) => if is_proj t then union (op =) (ixns, ixns') else ixns'
- | _ => union (op =) (ixns, ixns')))
+ SOME (SOME t) => if is_proj t then union (op =) ixns ixns' else ixns'
+ | _ => union (op =) ixns ixns'))
(needed prop ts'' prfs, add_npvars false true [] ([], prop));
val insts' = map
(fn (ixn, x as SOME _) => if member (op =) nvs ixn then (false, x) else (true, NONE)
| (_, x) => (false, x)) insts
in ([], false, insts' @ map (pair false) ts'', prf) end
and needed (Const ("==>", _) $ t $ u) ts ((b, _, _, _)::prfs) =
- union (op =) (if b then map (fst o dest_Var) (vars_of t) else [], needed u ts prfs)
+ union (op =) (if b then map (fst o dest_Var) (vars_of t) else []) (needed u ts prfs)
| needed (Var (ixn, _)) (_::_) _ = [ixn]
| needed _ _ _ = [];
in shrink end;
--- a/src/Tools/IsaPlanner/rw_inst.ML Wed Oct 21 10:15:31 2009 +0200
+++ b/src/Tools/IsaPlanner/rw_inst.ML Wed Oct 21 12:08:52 2009 +0200
@@ -139,13 +139,11 @@
val names = List.foldr OldTerm.add_term_names [] (tgt :: rule_conds);
val (conds_tyvs,cond_vs) =
Library.foldl (fn ((tyvs, vs), t) =>
- (union (op =)
- (OldTerm.term_tvars t, tyvs),
- union (op =)
- (map Term.dest_Var (OldTerm.term_vars t), vs)))
+ (union (op =) (OldTerm.term_tvars t) tyvs,
+ union (op =) (map Term.dest_Var (OldTerm.term_vars t)) vs))
(([],[]), rule_conds);
val termvars = map Term.dest_Var (OldTerm.term_vars tgt);
- val vars_to_fix = union (op =) (termvars, cond_vs);
+ val vars_to_fix = union (op =) termvars cond_vs;
val (renamings, names2) =
List.foldr (fn (((n,i),ty), (vs, names')) =>
let val n' = Name.variant names' n in