replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
--- a/NEWS Tue Oct 20 13:37:56 2009 +0200
+++ b/NEWS Tue Oct 20 16:13:01 2009 +0200
@@ -213,6 +213,9 @@
*** ML ***
+* Removed some old-style infix operations using polymorphic equality.
+INCOMPATIBILITY.
+
* Structure Synchronized (cf. src/Pure/Concurrent/synchronized.ML)
provides a high-level programming interface to synchronized state
variables with atomic update. This works via pure function
--- a/src/HOL/Import/proof_kernel.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/HOL/Import/proof_kernel.ML Tue Oct 20 16:13:01 2009 +0200
@@ -281,9 +281,10 @@
| itr (a::rst) = i=a orelse itr rst
in itr L end;
+infix union;
fun [] union S = S
| S union [] = S
- | (a::rst) union S2 = rst union (insert (op =) a S2)
+ | (a::rst) union S2 = rst union (insert (op =) a S2);
fun implode_subst [] = []
| implode_subst (x::r::rest) = ((x,r)::(implode_subst rest))
@@ -1229,7 +1230,7 @@
| add_consts (_, cs) = cs
val t_consts = add_consts(t,[])
in
- fn th => eq_set(t_consts,add_consts(prop_of th,[]))
+ fn th => gen_eq_set (op =) (t_consts, add_consts (prop_of th, []))
end
fun split_name str =
--- a/src/HOL/Import/shuffler.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/HOL/Import/shuffler.ML Tue Oct 20 16:13:01 2009 +0200
@@ -563,7 +563,7 @@
let
val th_consts = add_consts(prop_of th,[])
in
- eq_set(t_consts,th_consts)
+ gen_eq_set (op =) (t_consts, th_consts)
end
end
--- a/src/HOL/Nominal/nominal_primrec.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML Tue Oct 20 16:13:01 2009 +0200
@@ -228,7 +228,7 @@
(case Symtab.lookup dt_info tname of
NONE => primrec_err (quote tname ^ " is not a nominal datatype")
| SOME dt =>
- if tnames' subset (map (#1 o snd) (#descr dt)) then
+ if gen_subset (op =) (tnames', map (#1 o snd) (#descr dt)) then
(tname, dt)::(find_dts dt_info tnames' tnames)
else find_dts dt_info tnames' tnames);
@@ -251,7 +251,7 @@
val lsrs :: lsrss = maps (fn (_, (_, _, eqns)) =>
map (fn (_, (ls, _, rs, _, _)) => ls @ rs) eqns) eqns
val _ =
- (if forall (curry eq_set lsrs) lsrss andalso forall
+ (if forall (curry (gen_eq_set (op =)) lsrs) lsrss andalso forall
(fn (_, (_, _, (_, (ls, _, rs, _, _)) :: eqns)) =>
forall (fn (_, (ls', _, rs', _, _)) =>
ls = ls' andalso rs = rs') eqns
--- a/src/HOL/Set.thy Tue Oct 20 13:37:56 2009 +0200
+++ b/src/HOL/Set.thy Tue Oct 20 16:13:01 2009 +0200
@@ -303,7 +303,7 @@
fun check (Const ("Ex", _) $ Abs (_, _, P), n) = check (P, n + 1)
| check (Const ("op &", _) $ (Const ("op =", _) $ Bound m $ e) $ P, n) =
n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso
- ((0 upto (n - 1)) subset add_loose_bnos (e, 0, []))
+ gen_subset (op =) (0 upto (n - 1), add_loose_bnos (e, 0, []))
| check _ = false
fun tr' (_ $ abs) =
--- a/src/HOL/Tools/Datatype/datatype.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML Tue Oct 20 16:13:01 2009 +0200
@@ -489,7 +489,7 @@
val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
let val full_tname = Sign.full_name tmp_thy (Binding.map_name (Syntax.type_name mx) tname)
in (case duplicates (op =) tvs of
- [] => if eq_set (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
+ [] => if gen_eq_set (op =) (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
else error ("Mutually recursive datatypes must have same type parameters")
| dups => error ("Duplicate parameter(s) for datatype " ^ quote (Binding.str_of tname) ^
" : " ^ commas dups))
--- a/src/HOL/Tools/Datatype/datatype_aux.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML Tue Oct 20 16:13:01 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)) =>
- filter_out is_rec_type cargs union Ts') (Ts, constrs)) ([], descr));
+ gen_union (op =) (filter_out is_rec_type cargs, Ts')) (Ts, constrs)) ([], descr));
(* get all recursive types in datatype description *)
--- a/src/HOL/Tools/Function/context_tree.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/HOL/Tools/Function/context_tree.ML Tue Oct 20 16:13:01 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 (c1 inter t2)
+ if i = j orelse null (gen_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 Tue Oct 20 13:37:56 2009 +0200
+++ b/src/HOL/Tools/Function/pattern_split.ML Tue Oct 20 16:13:01 2009 +0200
@@ -101,7 +101,7 @@
let
val t = Pattern.rewrite_term thy sigma [] feq1
in
- fold_rev Logic.all (map Free (frees_in_term ctx t) inter vs') t
+ fold_rev Logic.all (gen_inter (op =) (map Free (frees_in_term ctx t), vs')) t
end
in
map instantiate substs
--- a/src/HOL/Tools/Groebner_Basis/groebner.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/HOL/Tools/Groebner_Basis/groebner.ML Tue Oct 20 16:13:01 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 =) ((map fst lis1) union (map fst lis2))
+ val dom = distinct (op =) (gen_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 Tue Oct 20 13:37:56 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Oct 20 16:13:01 2009 +0200
@@ -984,20 +984,20 @@
val dupTs = map snd (duplicates (op =) vTs) @
map_filter (AList.lookup (op =) vTs) vs;
in
- terms_vs (in_ts @ in_ts') subset vs andalso
+ gen_subset (op =) (terms_vs (in_ts @ in_ts'), vs) andalso
forall (is_eqT o fastype_of) in_ts' andalso
- term_vs t subset vs andalso
+ gen_subset (op =) (term_vs t, vs) andalso
forall is_eqT dupTs
end)
(modes_of_term modes t handle Option =>
error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
| Negprem (us, t) => find_first (fn Mode (_, is, _) =>
length us = length is andalso
- terms_vs us subset vs andalso
- term_vs t subset vs)
+ gen_subset (op =) (terms_vs us, vs) andalso
+ gen_subset (op =) (term_vs t, vs))
(modes_of_term modes t handle Option =>
error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
- | Sidecond t => if term_vs t subset vs then SOME (Mode (([], []), [], []))
+ | Sidecond t => if gen_subset (op =) (term_vs t, vs) then SOME (Mode (([], []), [], []))
else NONE
) ps);
@@ -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, _) => vs union terms_vs us | _ => vs)
+ (case p of Prem (us, _) => gen_union (op =) (vs, terms_vs us) | _ => vs)
(filter_out (equal p) ps)
| _ =>
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' (vs union generator_vs) ps)) all_generator_vs) of
+ (select_mode_prem thy modes' (gen_union (op =) (vs, generator_vs)) ps)) all_generator_vs) of
SOME generator_vs => check_mode_prems ((map (generator vTs) generator_vs) @ acc_ps)
- (vs union generator_vs) ps
+ (gen_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, _) => vs union terms_vs us | _ => vs)
+ (case p of Prem (us, _) => gen_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,13 +1073,13 @@
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 [] (param_vs union in_vs) ps of
+ case check_mode_prems [] (gen_union (op =) (param_vs, in_vs)) ps of
NONE => NONE
| SOME (acc_ps, vs) =>
if with_generator then
SOME (ts, (rev acc_ps) @ (map (generator vTs) (concl_vs \\ vs)))
else
- if concl_vs subset vs then SOME (ts, rev acc_ps) else NONE
+ if gen_subset (op =) (concl_vs, vs) then SOME (ts, rev acc_ps) else NONE
else NONE
end;
--- a/src/HOL/Tools/Qelim/cooper.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Tue Oct 20 16:13:01 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 (cs union ds)
+ val l = Integer.lcms (gen_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/inductive_codegen.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Tue Oct 20 16:13:01 2009 +0200
@@ -202,15 +202,15 @@
val dupTs = map snd (duplicates (op =) vTs) @
map_filter (AList.lookup (op =) vTs) vs;
in
- terms_vs (in_ts @ in_ts') subset vs andalso
+ gen_subset (op =) (terms_vs (in_ts @ in_ts'), vs) andalso
forall (is_eqT o fastype_of) in_ts' andalso
- term_vs t subset vs andalso
+ gen_subset (op =) (term_vs t, vs) andalso
forall is_eqT dupTs
end)
(if is_set then [Mode (([], []), [], [])]
else modes_of modes t handle Option =>
error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
- | Sidecond t => if term_vs t subset vs then SOME (Mode (([], []), [], []))
+ | Sidecond t => if gen_subset (op =) (term_vs t, vs) then SOME (Mode (([], []), [], []))
else NONE) ps);
fun check_mode_clause thy arg_vs modes (iss, is) (ts, ps) =
@@ -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, _, _) => vs union terms_vs us | _ => vs)
+ (case x of Prem (us, _, _) => gen_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,9 +230,9 @@
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 (arg_vs union in_vs) ps of
+ (case check_mode_prems (gen_union (op =) (arg_vs, in_vs)) ps of
NONE => false
- | SOME vs => concl_vs subset vs)
+ | SOME vs => gen_subset (op =) (concl_vs, vs))
end;
fun check_modes_pred thy arg_vs preds modes (p, ms) =
@@ -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' => xs inter xs') :: constrain cs ys;
+ | SOME xs' => gen_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 Tue Oct 20 13:37:56 2009 +0200
+++ b/src/HOL/Tools/inductive_set.ML Tue Oct 20 16:13:01 2009 +0200
@@ -209,7 +209,7 @@
(case optf of
NONE => fs
| SOME f => AList.update op = (u, the_default f
- (Option.map (curry op inter f) (AList.lookup op = fs u))) fs));
+ (Option.map (curry (gen_inter (op =)) f) (AList.lookup op = fs u))) fs));
(**************************************************************)
--- a/src/HOL/Tools/metis_tools.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/HOL/Tools/metis_tools.ML Tue Oct 20 16:13:01 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 = tfree_lits union tfrees}
+ tfrees = gen_union (op =) (tfree_lits, tfrees)}
end;
val lmap0 = List.foldl (add_thm true)
{axioms = [], tfrees = init_tfrees ctxt} cls
--- a/src/HOL/Tools/old_primrec.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/HOL/Tools/old_primrec.ML Tue Oct 20 16:13:01 2009 +0200
@@ -226,7 +226,7 @@
(case Symtab.lookup dt_info tname of
NONE => primrec_err (quote tname ^ " is not a datatype")
| SOME dt =>
- if tnames' subset (map (#1 o snd) (#descr dt)) then
+ if gen_subset (op =) (tnames', map (#1 o snd) (#descr dt)) then
(tname, dt)::(find_dts dt_info tnames' tnames)
else find_dts dt_info tnames' tnames);
--- a/src/HOL/Tools/primrec.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/HOL/Tools/primrec.ML Tue Oct 20 16:13:01 2009 +0200
@@ -208,7 +208,7 @@
(case Symtab.lookup dt_info tname of
NONE => primrec_error (quote tname ^ " is not a datatype")
| SOME dt =>
- if tnames' subset (map (#1 o snd) (#descr dt)) then
+ if gen_subset (op =) (tnames', map (#1 o snd) (#descr dt)) then
(tname, dt)::(find_dts dt_info tnames' tnames)
else find_dts dt_info tnames' tnames);
--- a/src/HOL/Tools/prop_logic.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/HOL/Tools/prop_logic.ML Tue Oct 20 16:13:01 2009 +0200
@@ -111,8 +111,8 @@
| indices False = []
| indices (BoolVar i) = [i]
| indices (Not fm) = indices fm
- | indices (Or (fm1, fm2)) = (indices fm1) union_int (indices fm2)
- | indices (And (fm1, fm2)) = (indices fm1) union_int (indices fm2);
+ | indices (Or (fm1, fm2)) = gen_union (op =) (indices fm1, indices fm2)
+ | indices (And (fm1, fm2)) = gen_union (op =) (indices fm1, indices fm2);
(* ------------------------------------------------------------------------- *)
(* maxidx: computes the maximal variable index occuring in a formula of *)
--- a/src/HOL/Tools/record.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/HOL/Tools/record.ML Tue Oct 20 16:13:01 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 = alphas inter alphas_fields;
+ val alphas_ext = gen_inter (op =) (alphas, alphas_fields);
val len = length fields;
val variants =
Name.variant_list (moreN :: rN :: (rN ^ "'") :: wN :: parent_variants)
--- a/src/HOL/Tools/refute.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/HOL/Tools/refute.ML Tue Oct 20 16:13:01 2009 +0200
@@ -1154,7 +1154,7 @@
val axioms = collect_axioms thy u
(* Term.typ list *)
val types = Library.foldl (fn (acc, t') =>
- acc union (ground_types thy t')) ([], u :: axioms)
+ gen_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)))
@@ -2415,7 +2415,7 @@
(#2 (the (AList.lookup (op =) descr idt_index)) ~~ (snd o dest_Type) IDT))
(* sanity check: typ_assoc must associate types to the *)
(* elements of 'dtyps' (and only to those) *)
- val _ = if not (Library.eq_set (dtyps, map fst typ_assoc))
+ val _ = if not (gen_eq_set (op =) (dtyps, map fst typ_assoc))
then
raise REFUTE ("IDT_recursion_interpreter",
"type association has extra/missing elements")
@@ -3007,7 +3007,7 @@
[Type ("fun", [T, Type ("bool", [])]),
Type ("fun", [_, Type ("bool", [])])]),
Type ("fun", [_, Type ("bool", [])])])) =>
- let nonfix union (* because "union" is used below *)
+ let
val size_elem = size_of_type thy model T
(* the universe (i.e. the set that contains every element) *)
val i_univ = Node (replicate size_elem TT)
--- a/src/HOL/Tools/res_atp.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/HOL/Tools/res_atp.ML Tue Oct 20 16:13:01 2009 +0200
@@ -213,8 +213,9 @@
fun defs lhs rhs =
let val (rator,args) = strip_comb lhs
val ct = const_with_typ thy (dest_ConstFree rator)
- in forall is_Var args andalso uni_mem gctypes ct andalso
- Term.add_vars rhs [] subset Term.add_vars lhs []
+ in
+ forall is_Var args andalso uni_mem gctypes ct andalso
+ gen_subset (op =) (Term.add_vars rhs [], Term.add_vars lhs [])
end
handle ConstFree => false
in
--- a/src/HOL/Tools/res_clause.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/HOL/Tools/res_clause.ML Tue Oct 20 16:13:01 2009 +0200
@@ -93,7 +93,7 @@
val tconst_prefix = "tc_";
val class_prefix = "class_";
-fun union_all xss = List.foldl (op union) [] xss;
+fun union_all xss = List.foldl (gen_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 (op union) [] (map sorts_on_typs Ts);
+fun add_typs Ts = List.foldl (gen_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
@@ -372,7 +372,7 @@
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 (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
- in (classes' union classes, cpairs' union cpairs) end;
+ in (gen_union (op =) (classes', classes), gen_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 Tue Oct 20 13:37:56 2009 +0200
+++ b/src/HOL/Tools/res_hol_clause.ML Tue Oct 20 16:13:01 2009 +0200
@@ -154,7 +154,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'), tsP union tsQ) end
+ in (CombApp(P',Q'), gen_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)
@@ -166,7 +166,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, ts union ts')
+ (Literal(pol,pred)::lits, gen_union (op =) (ts, ts'))
end;
fun literals_of_term_dfg dfg thy P = literals_of_term1 dfg thy ([],[]) P;
@@ -475,7 +475,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 (op union_string) [] tfree_litss)
+ val tfree_clss = map RC.tptp_tfree_clause (List.foldl (gen_union (op =)) [] tfree_litss)
val _ =
File.write_list file (
map (#1 o (clause2tptp params)) axclauses @
--- a/src/HOL/Tools/res_reconstruct.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML Tue Oct 20 16:13:01 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 (op union_int) [] (map (replace_dep (old, new)) deps));
+ (lno, t, List.foldl (gen_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 Tue Oct 20 13:37:56 2009 +0200
+++ b/src/HOL/Tools/sat_solver.ML Tue Oct 20 16:13:01 2009 +0200
@@ -471,8 +471,8 @@
| forced_vars False = []
| forced_vars (BoolVar i) = [i]
| forced_vars (Not (BoolVar i)) = [~i]
- | forced_vars (Or (fm1, fm2)) = (forced_vars fm1) inter_int (forced_vars fm2)
- | forced_vars (And (fm1, fm2)) = (forced_vars fm1) union_int (forced_vars fm2)
+ | forced_vars (Or (fm1, fm2)) = gen_inter (op =) (forced_vars fm1, forced_vars fm2)
+ | forced_vars (And (fm1, fm2)) = gen_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 Tue Oct 20 13:37:56 2009 +0200
+++ b/src/HOL/Tools/transfer.ML Tue Oct 20 16:13:01 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
- (hints1 union_string hints2)}
+ (gen_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 = hints1 union_string hints2}
+ {inj = h inj1 inj2, emb = h emb1 emb2, ret = h ret1 ret2, cong = h cg1 cg2, guess = g1 andalso g2, hints = gen_union (op =) (hints1, hints2)}
end;
fun add ((inja,injd), (emba,embd), (reta,retd), (cga,cgd), g, (hintsa, hintsd)) =
--- a/src/HOL/ex/predicate_compile.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML Tue Oct 20 16:13:01 2009 +0200
@@ -908,20 +908,20 @@
val dupTs = map snd (duplicates (op =) vTs) @
map_filter (AList.lookup (op =) vTs) vs;
in
- terms_vs (in_ts @ in_ts') subset vs andalso
+ gen_subset (op =) (terms_vs (in_ts @ in_ts'), vs) andalso
forall (is_eqT o fastype_of) in_ts' andalso
- term_vs t subset vs andalso
+ gen_subset (op =) (term_vs t, vs) andalso
forall is_eqT dupTs
end)
(modes_of_term modes t handle Option =>
error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
| Negprem (us, t) => find_first (fn Mode (_, is, _) =>
length us = length is andalso
- terms_vs us subset vs andalso
- term_vs t subset vs)
+ gen_subset (op =) (terms_vs us, vs) andalso
+ gen_subset (op =) (term_vs t, vs)
(modes_of_term modes t handle Option =>
error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
- | Sidecond t => if term_vs t subset vs then SOME (Mode (([], []), [], []))
+ | Sidecond t => if gen_subset (op =) (term_vs t, vs) then SOME (Mode (([], []), [], []))
else NONE
) ps);
@@ -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, _) => vs union terms_vs us | _ => vs)
+ (case p of Prem (us, _) => gen_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' (vs union generator_vs) ps)) all_generator_vs) of
+ (select_mode_prem thy modes' (gen_union (op =) (vs, generator_vs)) ps)) all_generator_vs) of
SOME generator_vs => check_mode_prems ((map (generator vTs) generator_vs) @ acc_ps)
- (vs union generator_vs) ps
+ (gen_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, _) => vs union terms_vs us | _ => vs)
+ (case p of Prem (us, _) => gen_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,13 +987,13 @@
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 [] (param_vs union in_vs) ps of
+ case check_mode_prems [] (gen_union (op =) (param_vs, in_vs)) ps of
NONE => NONE
| SOME (acc_ps, vs) =>
if with_generator then
SOME (ts, (rev acc_ps) @ (map (generator vTs) (concl_vs \\ vs)))
else
- if concl_vs subset vs then SOME (ts, rev acc_ps) else NONE
+ if gen_subset (op =) (concl_vs, vs) then SOME (ts, rev acc_ps) else NONE
else NONE
end;
--- a/src/HOLCF/Tools/Domain/domain_extender.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML Tue Oct 20 16:13:01 2009 +0200
@@ -59,8 +59,8 @@
fun analyse indirect (TFree(v,s)) =
(case AList.lookup (op =) tvars v of
NONE => error ("Free type variable " ^ quote v ^ " on rhs.")
- | SOME sort => if eq_set_string (s,defaultS) orelse
- eq_set_string (s,sort )
+ | SOME sort => if gen_eq_set (op =) (s, defaultS) orelse
+ gen_eq_set (op =) (s, sort)
then TFree(v,sort)
else error ("Inconsistent sort constraint" ^
" for type variable " ^ quote v))
--- a/src/Provers/Arith/cancel_div_mod.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/Provers/Arith/cancel_div_mod.ML Tue Oct 20 16:13:01 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 divs inter mods of
+ else case gen_inter (op =) (divs, mods) of
pq :: _ => SOME (cancel ss t pq)
| [] => NONE
end
--- a/src/Provers/Arith/fast_lin_arith.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Tue Oct 20 16:13:01 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 => l union cs) eqs []
+ fold (fn Lineq(_,_,l,_) => fn cs => gen_union (op =) (l, cs)) eqs []
|> filter (fn i => i <> 0)
|> sort (int_ord o pairself abs)
|> hd
--- a/src/Pure/General/name_space.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/Pure/General/name_space.ML Tue Oct 20 16:13:01 2009 +0200
@@ -145,7 +145,7 @@
space
|> add_name' name name
|> fold (del_name name)
- (if fully then names else names inter_string [Long_Name.base_name name])
+ (if fully then names else gen_inter (op =) (names, [Long_Name.base_name name]))
|> fold (del_name_extra name) (get_accesses space name)
end;
--- a/src/Pure/General/ord_list.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/Pure/General/ord_list.ML Tue Oct 20 16:13:01 2009 +0200
@@ -56,7 +56,6 @@
(* lists as sets *)
-nonfix subset;
fun subset ord (list1, list2) =
let
fun sub [] _ = true
@@ -75,7 +74,6 @@
fun handle_same f x = f x handle SAME => x;
(*union: insert elements of first list into second list*)
-nonfix union;
fun union ord list1 list2 =
let
fun unio [] _ = raise SAME
@@ -88,7 +86,6 @@
in if pointer_eq (list1, list2) then list1 else handle_same (unio list1) list2 end;
(*intersection: filter second list for elements present in first list*)
-nonfix inter;
fun inter ord list1 list2 =
let
fun intr _ [] = raise SAME
--- a/src/Pure/General/path.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/Pure/General/path.ML Tue Oct 20 16:13:01 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_string chs of
+ (case gen_inter (op =) (["/", "\\", "$", ":"], chs) of
[] => chs
| bads => err_elem ("Illegal character(s) " ^ commas_quote bads ^ " in") chs);
--- a/src/Pure/Proof/reconstruct.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/Pure/Proof/reconstruct.ML Tue Oct 20 16:13:01 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, op union
+ val cs' = map (fn p => (true, p, gen_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/ProofGeneral/pgip_parser.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/Pure/ProofGeneral/pgip_parser.ML Tue Oct 20 16:13:01 2009 +0200
@@ -77,7 +77,7 @@
|> command K.prf_asm_goal goal
|> command K.prf_script proofstep;
-val _ = OuterKeyword.kinds subset_string Symtab.keys command_keywords
+val _ = gen_subset (op =) (OuterKeyword.kinds, Symtab.keys command_keywords)
orelse sys_error "Incomplete coverage of command keywords";
fun parse_command "sorry" text = [D.Postponegoal {text = text}, D.Closeblock {}]
--- a/src/Pure/Syntax/ast.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/Pure/Syntax/ast.ML Tue Oct 20 16:13:01 2009 +0200
@@ -104,7 +104,7 @@
val rvars = add_vars rhs [];
in
if has_duplicates (op =) lvars then SOME "duplicate vars in lhs"
- else if not (rvars subset lvars) then SOME "rhs contains extra variables"
+ else if not (gen_subset (op =) (rvars, lvars)) then SOME "rhs contains extra variables"
else NONE
end;
--- a/src/Pure/Syntax/parser.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/Pure/Syntax/parser.ML Tue Oct 20 16:13:01 2009 +0200
@@ -147,7 +147,7 @@
in
if member (op =) nts l then (*update production's lookahead*)
let
- val new_lambda = is_none tk andalso nts subset lambdas;
+ val new_lambda = is_none tk andalso gen_subset (op =) (nts, lambdas);
val new_tks = subtract (op =) l_starts
((if is_some tk then [the tk] else []) @
--- a/src/Pure/Syntax/syn_ext.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/Pure/Syntax/syn_ext.ML Tue Oct 20 16:13:01 2009 +0200
@@ -352,7 +352,7 @@
in
SynExt {
xprods = xprods,
- consts = consts union_string mfix_consts,
+ consts = gen_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/Tools/find_theorems.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/Pure/Tools/find_theorems.ML Tue Oct 20 16:13:01 2009 +0200
@@ -227,7 +227,7 @@
fun check (t, NONE) = check (t, SOME (get_thm_names t))
| check ((_, thm), c as SOME thm_consts) =
- (if pat_consts subset_string thm_consts andalso
+ (if gen_subset (op =) (pat_consts, thm_consts) andalso
Pattern.matches_subterm (ProofContext.theory_of ctxt) (pat, Thm.full_prop_of thm)
then SOME (0, 0) else NONE, c);
in check end;
--- a/src/Pure/codegen.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/Pure/codegen.ML Tue Oct 20 16:13:01 2009 +0200
@@ -599,8 +599,8 @@
else Pretty.block (separate (Pretty.brk 1) (p :: ps));
fun new_names t xs = Name.variant_list
- (map (fst o fst o dest_Var) (OldTerm.term_vars t) union
- OldTerm.add_term_names (t, ML_Syntax.reserved_names)) (map mk_id xs);
+ (gen_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 Tue Oct 20 13:37:56 2009 +0200
+++ b/src/Pure/library.ML Tue Oct 20 16:13:01 2009 +0200
@@ -11,8 +11,7 @@
infix 2 ?
infix 3 o oo ooo oooo
infix 4 ~~ upto downto
-infix orf andf \ \\ mem mem_int mem_string union union_int
- union_string inter inter_int inter_string subset subset_int subset_string
+infix orf andf \ \\ mem mem_int mem_string
signature BASIC_LIBRARY =
sig
@@ -163,19 +162,8 @@
val mem: ''a * ''a list -> bool
val mem_int: int * int list -> bool
val mem_string: string * string list -> bool
- val union: ''a list * ''a list -> ''a list
- val union_int: int list * int list -> int list
- val union_string: string list * string list -> string list
val gen_union: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
val gen_inter: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list
- val inter: ''a list * ''a list -> ''a list
- val inter_int: int list * int list -> int list
- val inter_string: string list * string list -> string list
- val subset: ''a list * ''a list -> bool
- val subset_int: int list * int list -> bool
- val subset_string: string list * string list -> bool
- val eq_set: ''a list * ''a list -> bool
- val eq_set_string: string list * string list -> bool
val gen_subset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
val gen_eq_set: ('a * 'b -> bool) -> 'a list * 'b list -> bool
val \ : ''a list * ''a -> ''a list
@@ -811,70 +799,20 @@
fun (x: string) mem_string xs = member (op =) xs x;
(*union of sets represented as lists: no repetitions*)
-fun xs union [] = xs
- | [] union ys = ys
- | (x :: xs) union ys = xs union (insert (op =) x ys);
-
-(*union of sets, optimized version for ints*)
-fun (xs:int list) union_int [] = xs
- | [] union_int ys = ys
- | (x :: xs) union_int ys = xs union_int (insert (op =) x ys);
-
-(*union of sets, optimized version for strings*)
-fun (xs:string list) union_string [] = xs
- | [] union_string ys = ys
- | (x :: xs) union_string ys = xs union_string (insert (op =) x ys);
-
-(*generalized union*)
fun gen_union eq (xs, []) = xs
| gen_union eq ([], ys) = ys
| gen_union eq (x :: xs, ys) = gen_union eq (xs, insert eq x ys);
-
(*intersection*)
-fun [] inter ys = []
- | (x :: xs) inter ys =
- if x mem ys then x :: (xs inter ys) else xs inter ys;
-
-(*intersection, optimized version for ints*)
-fun ([]:int list) inter_int ys = []
- | (x :: xs) inter_int ys =
- if x mem_int ys then x :: (xs inter_int ys) else xs inter_int ys;
-
-(*intersection, optimized version for strings *)
-fun ([]:string list) inter_string ys = []
- | (x :: xs) inter_string ys =
- if x mem_string ys then x :: (xs inter_string ys) else xs inter_string ys;
-
-(*generalized intersection*)
fun gen_inter eq ([], ys) = []
| gen_inter eq (x::xs, ys) =
if member eq ys x then x :: gen_inter eq (xs, ys)
else gen_inter eq (xs, ys);
-
(*subset*)
-fun [] subset ys = true
- | (x :: xs) subset ys = x mem ys andalso xs subset ys;
-
-(*subset, optimized version for ints*)
-fun ([]: int list) subset_int ys = true
- | (x :: xs) subset_int ys = x mem_int ys andalso xs subset_int ys;
-
-(*subset, optimized version for strings*)
-fun ([]: string list) subset_string ys = true
- | (x :: xs) subset_string ys = x mem_string ys andalso xs subset_string ys;
+fun gen_subset eq (xs, ys) = forall (member eq ys) xs;
(*set equality*)
-fun eq_set (xs, ys) =
- xs = ys orelse (xs subset ys andalso ys subset xs);
-
-(*set equality for strings*)
-fun eq_set_string ((xs: string list), ys) =
- xs = ys orelse (xs subset_string ys andalso ys subset_string xs);
-
-fun gen_subset eq (xs, ys) = forall (member eq ys) xs;
-
fun gen_eq_set eq (xs, ys) =
eq_list eq (xs, ys) orelse
(gen_subset eq (xs, ys) andalso gen_subset (eq o swap) (ys, xs));
--- a/src/Pure/meta_simplifier.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/Pure/meta_simplifier.ML Tue Oct 20 16:13:01 2009 +0200
@@ -864,7 +864,7 @@
while the premises are solved.*)
fun cond_skel (args as (_, (lhs, rhs))) =
- if Term.add_vars rhs [] subset Term.add_vars lhs [] then uncond_skel args
+ if gen_subset (op =) (Term.add_vars rhs [], Term.add_vars lhs []) then uncond_skel args
else skel0;
(*
--- a/src/Pure/pattern.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/Pure/pattern.ML Tue Oct 20 16:13:01 2009 +0200
@@ -216,10 +216,10 @@
fun flexflex2(env,binders,F,Fty,is,G,Gty,js) =
let fun ff(F,Fty,is,G as (a,_),Gty,js) =
- if js subset_int is
+ if gen_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 = is inter_int js
+ else let val ks = gen_inter (op =) (is, js)
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));
@@ -339,7 +339,7 @@
let val js = loose_bnos t
in if null is
then if null js then Vartab.update_new (ixn, (T, t)) itms else raise MATCH
- else if js subset_int is
+ else if gen_subset (op =) (js, is)
then let val t' = if downto0(is,length binders - 1) then t
else mapbnd (idx is) t
in Vartab.update_new (ixn, (T, mkabs (binders, is, t'))) itms end
--- a/src/Pure/proofterm.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/Pure/proofterm.ML Tue Oct 20 16:13:01 2009 +0200
@@ -900,8 +900,8 @@
fun add_funvars Ts (vs, t) =
if is_fun (fastype_of1 (Ts, t)) then
- vs union map_filter (fn Var (ixn, T) =>
- if is_fun T then SOME ixn else NONE | _ => NONE) (vars_of t)
+ gen_union (op =) (vs, map_filter (fn Var (ixn, T) =>
+ if is_fun T then SOME ixn else NONE | _ => NONE) (vars_of t))
else vs;
fun add_npvars q p Ts (vs, Const ("==>", _) $ t $ u) =
@@ -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) = prop_vars P union prop_vars Q
+fun prop_vars (Const ("==>", _) $ P $ Q) = gen_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 =
- Library.foldl (op union)
- ([], map (uncurry (insert (op =))) (add_npvars true true [] ([], prop))) union
- prop_vars prop;
+ gen_union (op =) (Library.foldl (gen_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 (is union is', ch orelse ch', ts',
+ in (gen_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 ixns union ixns' else ixns'
- | _ => ixns union ixns'))
+ SOME (SOME t) => if is_proj t then gen_union (op =) (ixns, ixns') else ixns'
+ | _ => gen_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) =
- (if b then map (fst o dest_Var) (vars_of t) else []) union needed u ts prfs
+ gen_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/Pure/sorts.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/Pure/sorts.ML Tue Oct 20 16:13:01 2009 +0200
@@ -72,8 +72,8 @@
(** ordered lists of sorts **)
val make = OrdList.make TermOrd.sort_ord;
-val op subset = OrdList.subset TermOrd.sort_ord;
-val op union = OrdList.union TermOrd.sort_ord;
+val subset = OrdList.subset TermOrd.sort_ord;
+val union = OrdList.union TermOrd.sort_ord;
val subtract = OrdList.subtract TermOrd.sort_ord;
val remove_sort = OrdList.remove TermOrd.sort_ord;
--- a/src/Pure/thm.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/Pure/thm.ML Tue Oct 20 16:13:01 2009 +0200
@@ -1463,7 +1463,7 @@
(case duplicates (op =) cs of
a :: _ => (warning ("Can't rename. Bound variables not distinct: " ^ a); state)
| [] =>
- (case cs inter_string freenames of
+ (case gen_inter (op =) (cs, freenames) of
a :: _ => (warning ("Can't rename. Bound/Free variable clash: " ^ a); state)
| [] =>
Thm (der,
--- a/src/Pure/variable.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/Pure/variable.ML Tue Oct 20 16:13:01 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 (xs inter_string ys); no_dups (xs inter_string zs);
+ else (no_dups (gen_inter (op =) (xs, ys)); no_dups (gen_inter (op =) (xs, zs));
(xs, fold Name.declare xs names));
in ctxt |> new_fixes names' xs xs' end;
--- a/src/Tools/IsaPlanner/rw_inst.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/Tools/IsaPlanner/rw_inst.ML Tue Oct 20 16:13:01 2009 +0200
@@ -139,13 +139,13 @@
val names = List.foldr OldTerm.add_term_names [] (tgt :: rule_conds);
val (conds_tyvs,cond_vs) =
Library.foldl (fn ((tyvs, vs), t) =>
- (Library.union
+ (gen_union (op =)
(OldTerm.term_tvars t, tyvs),
- Library.union
+ gen_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 = Library.union (termvars, cond_vs);
+ val vars_to_fix = gen_union (op =) (termvars, cond_vs);
val (renamings, names2) =
List.foldr (fn (((n,i),ty), (vs, names')) =>
let val n' = Name.variant names' n in
--- a/src/Tools/Metis/metis_env.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/Tools/Metis/metis_env.ML Tue Oct 20 16:13:01 2009 +0200
@@ -1,5 +1,5 @@
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
--- a/src/ZF/Tools/primrec_package.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/ZF/Tools/primrec_package.ML Tue Oct 20 16:13:01 2009 +0200
@@ -65,7 +65,7 @@
in
if has_duplicates (op =) lfrees then
raise RecError "repeated variable name in pattern"
- else if not ((map dest_Free (OldTerm.term_frees rhs)) subset lfrees) then
+ else if not (gen_subset (op =) (Term.add_frees rhs [], lfrees)) then
raise RecError "extra variables on rhs"
else if length middle > 1 then
raise RecError "more than one non-variable in pattern"