# HG changeset patch # User haftmann # Date 1160481553 -7200 # Node ID 868120282837fea48ebd5f68afe97d13b16a2803 # Parent 981fa0ce23ed7e9b49210c7a7cead90865169af0 gen_rem(s) abandoned in favour of remove / subtract diff -r 981fa0ce23ed -r 868120282837 NEWS --- 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" diff -r 981fa0ce23ed -r 868120282837 TFL/rules.ML --- 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 (*-------------------------------------------------------------- diff -r 981fa0ce23ed -r 868120282837 TFL/tfl.ML --- 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 diff -r 981fa0ce23ed -r 868120282837 src/FOLP/simp.ML --- 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} diff -r 981fa0ce23ed -r 868120282837 src/HOL/Import/shuffler.ML --- 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' diff -r 981fa0ce23ed -r 868120282837 src/HOL/Library/EfficientNat.thy --- 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 diff -r 981fa0ce23ed -r 868120282837 src/HOL/Tools/inductive_realizer.ML --- 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 = diff -r 981fa0ce23ed -r 868120282837 src/HOL/Tools/recfun_codegen.ML --- 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 diff -r 981fa0ce23ed -r 868120282837 src/HOL/Tools/record_package.ML --- 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]); diff -r 981fa0ce23ed -r 868120282837 src/Pure/Isar/locale.ML --- 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; diff -r 981fa0ce23ed -r 868120282837 src/Pure/Syntax/parser.ML --- 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) diff -r 981fa0ce23ed -r 868120282837 src/Pure/library.ML --- 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 **) diff -r 981fa0ce23ed -r 868120282837 src/Pure/proof_general.ML --- 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 diff -r 981fa0ce23ed -r 868120282837 src/Pure/type.ML --- 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')) diff -r 981fa0ce23ed -r 868120282837 src/Sequents/prover.ML --- 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;