--- a/NEWS Tue Oct 10 13:59:12 2006 +0200
+++ b/NEWS Tue Oct 10 13:59:13 2006 +0200
@@ -632,6 +632,14 @@
* Pure/library:
+gen_rem(s) abandoned in favour of remove / subtract.
+INCOMPATIBILITY:
+rewrite "gen_rem eq (xs, x)" to "remove (eq o swap) x xs"
+rewrite "gen_rems eq (xs, ys)" to "subtract (eq o swap) ys xs"
+drop "swap" if "eq" is symmetric.
+
+* Pure/library:
+
infixes ins ins_string ins_int have been abandoned in favour of insert.
INCOMPATIBILITY: rewrite "x ins(_...) xs" to "insert (op =) x xs"
--- a/TFL/rules.ML Tue Oct 10 13:59:12 2006 +0200
+++ b/TFL/rules.ML Tue Oct 10 13:59:13 2006 +0200
@@ -763,8 +763,8 @@
val dummy = print_thms "cntxt:" cntxt
val {prop = Const("==>",_) $ (Const("Trueprop",_) $ A) $ _,
sign,...} = rep_thm thm
- fun genl tm = let val vlist = gen_rems (op aconv)
- (add_term_frees(tm,[]), globals)
+ fun genl tm = let val vlist = subtract (op aconv) globals
+ (add_term_frees(tm,[]))
in fold_rev Forall vlist tm
end
(*--------------------------------------------------------------
--- a/TFL/tfl.ML Tue Oct 10 13:59:12 2006 +0200
+++ b/TFL/tfl.ML Tue Oct 10 13:59:13 2006 +0200
@@ -767,7 +767,7 @@
of [] => (P_y, (tm,[]))
| _ => let
val imp = S.list_mk_conj cntxt ==> P_y
- val lvs = gen_rems (op aconv) (S.free_vars_lr imp, globals)
+ val lvs = subtract (op aconv) globals (S.free_vars_lr imp)
val locals = #2(U.pluck (curry (op aconv) P) lvs) handle U.ERR _ => lvs
in (S.list_mk_forall(locals,imp), (tm,locals)) end
end
@@ -994,7 +994,7 @@
fun loop ([],extras,R,ind) = (rev R, ind, extras)
| loop ((r,ftcs)::rst, nthms, R, ind) =
let val tcs = #1(strip_imp (concl r))
- val extra_tcs = gen_rems (op aconv) (ftcs, tcs)
+ val extra_tcs = subtract (op aconv) tcs ftcs
val extra_tc_thms = map simplify_nested_tc extra_tcs
val (r1,ind1) = fold simplify_tc tcs (r,ind)
val r2 = R.FILTER_DISCH_ALL(not o S.is_WFR) r1
--- a/src/FOLP/simp.ML Tue Oct 10 13:59:12 2006 +0200
+++ b/src/FOLP/simp.ML Tue Oct 10 13:59:13 2006 +0200
@@ -282,7 +282,7 @@
val delete_thms = foldr delete_thm_warn;
fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) =
-let val congs' = Library.foldl (gen_rem Drule.eq_thm_prop) (congs,thms)
+let val congs' = fold (remove Drule.eq_thm_prop) thms congs
in SS{auto_tac=auto_tac, congs= congs',
cong_net= delete_thms cong_net (map mk_trans thms),
mk_simps= normed_rews congs', simps=simps, simp_net=simp_net}
--- a/src/HOL/Import/shuffler.ML Tue Oct 10 13:59:12 2006 +0200
+++ b/src/HOL/Import/shuffler.ML Tue Oct 10 13:59:13 2006 +0200
@@ -270,7 +270,7 @@
val cU = ctyp_of sg U
val tfrees = add_term_tfrees (prop_of thm,[])
val (rens, thm') = Thm.varifyT'
- (gen_rem (op = o apfst fst) (tfrees, name)) thm
+ (remove (op = o apsnd fst) name tfrees) thm
val mid =
case rens of
[] => thm'
--- a/src/HOL/Library/EfficientNat.thy Tue Oct 10 13:59:12 2006 +0200
+++ b/src/HOL/Library/EfficientNat.thy Tue Oct 10 13:59:13 2006 +0200
@@ -258,7 +258,7 @@
[] => NONE
| thps =>
let val (ths1, ths2) = split_list thps
- in SOME (gen_rems eq_thm (thms, th :: ths1) @ ths2) end
+ in SOME (subtract eq_thm (th :: ths1) thms @ ths2) end
end
in
case get_first mk_thms eqs of
--- a/src/HOL/Tools/inductive_realizer.ML Tue Oct 10 13:59:12 2006 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Tue Oct 10 13:59:13 2006 +0200
@@ -262,7 +262,7 @@
val vs1 = map Var (filter_out (fn ((a, _), _) => a mem rvs) xs);
val rlzvs = rev (Term.add_vars (prop_of rrule) []);
val vs2 = map (fn (ixn, _) => Var (ixn, (the o AList.lookup (op =) rlzvs) ixn)) xs;
- val rs = gen_rems (op = o pairself fst) (rlzvs, xs);
+ val rs = subtract (op = o pairself fst) xs rlzvs;
fun mk_prf _ [] prf = prf
| mk_prf rs ((prem, rprem) :: prems) prf =
--- a/src/HOL/Tools/recfun_codegen.ML Tue Oct 10 13:59:12 2006 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML Tue Oct 10 13:59:13 2006 +0200
@@ -56,7 +56,7 @@
in case Symtab.lookup tab s of
NONE => thy
| SOME thms =>
- RecCodegenData.put (Symtab.update (s, gen_rem (eq_thm o apfst fst) (thms, thm)) tab) thy
+ RecCodegenData.put (Symtab.update (s, remove (eq_thm o apsnd fst) thm thms) tab) thy
end handle TERM _ => (warn thm; thy);
val del = Thm.declaration_attribute
--- a/src/HOL/Tools/record_package.ML Tue Oct 10 13:59:12 2006 +0200
+++ b/src/HOL/Tools/record_package.ML Tue Oct 10 13:59:13 2006 +0200
@@ -2078,7 +2078,7 @@
| dups => ["Duplicate parameter(s) " ^ commas dups]);
val err_extra_frees =
- (case gen_rems (op =) (envir_names, params) of
+ (case subtract (op =) params envir_names of
[] => []
| extras => ["Extra free type variable(s) " ^ commas extras]);
--- a/src/Pure/Isar/locale.ML Tue Oct 10 13:59:12 2006 +0200
+++ b/src/Pure/Isar/locale.ML Tue Oct 10 13:59:13 2006 +0200
@@ -851,7 +851,7 @@
val all_params = map (fn p => (p, Symtab.lookup tenv p |> the)) all_params';
(* compute identifiers and syntax, merge with previous ones *)
val (ids, _) = identify true expr;
- val idents = gen_rems (eq_fst (op =)) (ids, prev_idents);
+ val idents = subtract (eq_fst (op =)) prev_idents ids;
val syntax = merge_syntax ctxt ids (syn, prev_syntax);
(* type-instantiate elements *)
val final_elemss = map (eval all_params tenv syntax) idents;
--- a/src/Pure/Syntax/parser.ML Tue Oct 10 13:59:12 2006 +0200
+++ b/src/Pure/Syntax/parser.ML Tue Oct 10 13:59:13 2006 +0200
@@ -259,7 +259,7 @@
let
val ((old_nts, old_tks), nt_prods) = Array.sub (prods, nt);
- val new_tks = gen_rems matching_tokens (start_tks, old_tks);
+ val new_tks = subtract matching_tokens old_tks start_tks;
(*store new production*)
fun store [] prods is_new =
@@ -370,7 +370,7 @@
|> (K (key = SOME UnknownStart)) ? AList.update (op =) (key, tk_prods')
val added_tks =
- gen_rems matching_tokens (new_tks, old_tks);
+ subtract matching_tokens old_tks new_tks;
in if null added_tks then
(Array.update (prods, nt, (lookahead, nt_prods'));
process_nts nts added)
--- a/src/Pure/library.ML Tue Oct 10 13:59:12 2006 +0200
+++ b/src/Pure/library.ML Tue Oct 10 13:59:13 2006 +0200
@@ -219,8 +219,6 @@
val gen_eq_set: ('a * 'b -> bool) -> 'a list * 'b list -> bool
val \ : ''a list * ''a -> ''a list
val \\ : ''a list * ''a list -> ''a list
- val gen_rem: ('a * 'b -> bool) -> 'a list * 'b -> 'a list
- val gen_rems: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list
val findrep: ''a list -> ''a list
val distinct: ('a * 'a -> bool) -> 'a list -> 'a list
val duplicates: ('a * 'a -> bool) -> 'a list -> 'a list
@@ -1035,12 +1033,8 @@
(*removing an element from a list WITHOUT duplicates*)
fun (y :: ys) \ x = if x = y then ys else y :: (ys \ x)
| [] \ x = [];
-
fun ys \\ xs = foldl (op \) (ys,xs);
-(*removing an element from a list -- possibly WITH duplicates*)
-fun gen_rem eq (xs, y) = filter_out (fn x => eq (x, y)) xs;
-fun gen_rems eq (xs, ys) = filter_out (member eq ys) xs;
(*returns the tail beginning with the first repeated element, or []*)
fun findrep [] = []
@@ -1079,10 +1073,10 @@
fun gen_merge_lists _ xs [] = xs
| gen_merge_lists _ [] ys = ys
- | gen_merge_lists eq xs ys = xs @ gen_rems eq (ys, xs);
+ | gen_merge_lists eq xs ys = xs @ filter_out (member eq xs) ys;
fun merge_lists xs ys = gen_merge_lists (op =) xs ys;
-fun merge_alists al = gen_merge_lists (eq_fst (op =)) al;
+fun merge_alists xs = gen_merge_lists (eq_fst (op =)) xs;
(** balanced trees **)
--- a/src/Pure/proof_general.ML Tue Oct 10 13:59:12 2006 +0200
+++ b/src/Pure/proof_general.ML Tue Oct 10 13:59:13 2006 +0200
@@ -385,7 +385,7 @@
fun add_master_files name files =
let val masters = [ThyLoad.thy_path name, ThyLoad.ml_path name]
- in masters @ gen_rems (op = o pairself Path.base) (files, masters) end;
+ in masters @ subtract (op = o pairself Path.base) masters files end;
fun trace_action action name =
if action = ThyInfo.Update then
--- a/src/Pure/type.ML Tue Oct 10 13:59:12 2006 +0200
+++ b/src/Pure/type.ML Tue Oct 10 13:59:13 2006 +0200
@@ -552,7 +552,7 @@
(case duplicates (op =) vs of
[] => []
| dups => err ("Duplicate variables on lhs: " ^ commas_quote dups));
- (case gen_rems (op =) (map (#1 o #1) (typ_tvars rhs'), vs) of
+ (case subtract (op =) vs (map (#1 o #1) (typ_tvars rhs')) of
[] => []
| extras => err ("Extra variables on rhs: " ^ commas_quote extras));
types |> new_decl naming (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs'))
--- a/src/Sequents/prover.ML Tue Oct 10 13:59:12 2006 +0200
+++ b/src/Sequents/prover.ML Tue Oct 10 13:59:13 2006 +0200
@@ -33,14 +33,14 @@
fun (Pack(safes,unsafes)) add_safes ths =
let val dups = warn_duplicates (gen_inter Drule.eq_thm_prop (ths,safes))
- val ths' = gen_rems Drule.eq_thm_prop (ths,dups)
+ val ths' = subtract Drule.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 (gen_inter Drule.eq_thm_prop (ths,unsafes))
- val ths' = gen_rems Drule.eq_thm_prop (ths,dups)
+ val ths' = subtract Drule.eq_thm_prop dups ths
in
Pack(safes, sort (make_ord less) (ths'@unsafes))
end;