# HG changeset patch # User wenzelm # Date 1256835506 -3600 # Node ID b4534348b8fd3176d92cf087c18b4ca54704cc27 # Parent 6a72af4e84b8e38650bb2e97a063e908867b565d standardized filter/filter_out; diff -r 6a72af4e84b8 -r b4534348b8fd src/CCL/Wfd.thy --- a/src/CCL/Wfd.thy Thu Oct 29 16:59:12 2009 +0100 +++ b/src/CCL/Wfd.thy Thu Oct 29 17:58:26 2009 +0100 @@ -440,7 +440,7 @@ fun IHinst tac rls = SUBGOAL (fn (Bi,i) => let val bvs = bvars Bi [] - val ihs = List.filter could_IH (Logic.strip_assums_hyp Bi) + val ihs = filter could_IH (Logic.strip_assums_hyp Bi) val rnames = map (fn x=> let val (a,b) = get_bno [] 0 x in (List.nth(bvs,a),b) end) ihs diff -r 6a72af4e84b8 -r b4534348b8fd src/FOLP/simp.ML --- a/src/FOLP/simp.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/FOLP/simp.ML Thu Oct 29 17:58:26 2009 +0100 @@ -215,7 +215,7 @@ fun add_norm_tags congs = let val ccs = map cong_const congs - val new_asms = List.filter (exists not o #2) + val new_asms = filter (exists not o #2) (ccs ~~ (map (map atomic o prems_of) congs)); in add_norms(congs,ccs,new_asms) end; diff -r 6a72af4e84b8 -r b4534348b8fd src/HOL/Import/import_syntax.ML --- a/src/HOL/Import/import_syntax.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/HOL/Import/import_syntax.ML Thu Oct 29 17:58:26 2009 +0100 @@ -61,7 +61,7 @@ val thyname = get_generating_thy thy val segname = get_import_segment thy val (int_thms,facts) = Replay.setup_int_thms thyname thy - val thmnames = List.filter (not o should_ignore thyname thy) facts + val thmnames = filter_out (should_ignore thyname thy) facts fun replay thy = let val _ = ImportRecorder.load_history thyname diff -r 6a72af4e84b8 -r b4534348b8fd src/HOL/Import/shuffler.ML --- a/src/HOL/Import/shuffler.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/HOL/Import/shuffler.ML Thu Oct 29 17:58:26 2009 +0100 @@ -628,7 +628,7 @@ val all_thms = map (`Thm.get_name_hint) (maps #2 (Facts.dest_static [] (PureThy.facts_of thy))) in - List.filter (match_consts ignored t) all_thms + filter (match_consts ignored t) all_thms end fun gen_shuffle_tac ctxt search thms i st = diff -r 6a72af4e84b8 -r b4534348b8fd src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/HOL/Nominal/nominal_datatype.ML Thu Oct 29 17:58:26 2009 +0100 @@ -66,7 +66,7 @@ fun mk_case_names_exhausts descr new = map (RuleCases.case_names o exhaust_cases descr o #1) - (List.filter (fn ((_, (name, _, _))) => name mem_string new) descr); + (filter (fn ((_, (name, _, _))) => name mem_string new) descr); end; @@ -1166,11 +1166,11 @@ fun make_ind_prem fsT f k T ((cname, cargs), idxs) = let - val recs = List.filter is_rec_type cargs; + val recs = filter is_rec_type cargs; val Ts = map (typ_of_dtyp descr'' sorts) cargs; val recTs' = map (typ_of_dtyp descr'' sorts) recs; val tnames = Name.variant_list pnames (DatatypeProp.make_tnames Ts); - val rec_tnames = map fst (List.filter (is_rec_type o snd) (tnames ~~ cargs)); + val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs)); val frees = tnames ~~ Ts; val frees' = partition_cargs idxs frees; val z = (Name.variant tnames "z", fsT); diff -r 6a72af4e84b8 -r b4534348b8fd src/HOL/Nominal/nominal_primrec.ML --- a/src/HOL/Nominal/nominal_primrec.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/HOL/Nominal/nominal_primrec.ML Thu Oct 29 17:58:26 2009 +0100 @@ -193,7 +193,7 @@ NONE => let val dummy_fns = map (fn (_, cargs) => Const (@{const_name undefined}, - replicate ((length cargs) + (length (List.filter is_rec_type cargs))) + replicate (length cargs + length (filter is_rec_type cargs)) dummyT ---> HOLogic.unitT)) constrs; val _ = warning ("No function definition for datatype " ^ quote tname) in diff -r 6a72af4e84b8 -r b4534348b8fd src/HOL/Tools/Datatype/datatype_abs_proofs.ML --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Thu Oct 29 17:58:26 2009 +0100 @@ -292,7 +292,7 @@ val case_dummy_fns = map (fn (_, (_, _, constrs)) => map (fn (_, cargs) => let val Ts = map (typ_of_dtyp descr' sorts) cargs; - val Ts' = map mk_dummyT (List.filter is_rec_type cargs) + val Ts' = map mk_dummyT (filter is_rec_type cargs) in Const (@{const_name undefined}, Ts @ Ts' ---> T') end) constrs) descr'; @@ -305,7 +305,7 @@ val (fns1, fns2) = split_list (map (fn ((_, cargs), j) => let val Ts = map (typ_of_dtyp descr' sorts) cargs; - val Ts' = Ts @ map mk_dummyT (List.filter is_rec_type cargs); + val Ts' = Ts @ map mk_dummyT (filter is_rec_type cargs); val frees' = map (uncurry (mk_Free "x")) (Ts' ~~ (1 upto length Ts')); val frees = Library.take (length cargs, frees'); val free = mk_Free "f" (Ts ---> T') j diff -r 6a72af4e84b8 -r b4534348b8fd src/HOL/Tools/Datatype/datatype_aux.ML --- a/src/HOL/Tools/Datatype/datatype_aux.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML Thu Oct 29 17:58:26 2009 +0100 @@ -231,7 +231,7 @@ fun name_of_typ (Type (s, Ts)) = let val s' = Long_Name.base_name s - in space_implode "_" (List.filter (not o equal "") (map name_of_typ Ts) @ + in space_implode "_" (filter_out (equal "") (map name_of_typ Ts) @ [if Syntax.is_identifier s' then s' else "x"]) end | name_of_typ _ = ""; @@ -272,7 +272,7 @@ fun get_arities descr = fold (fn (_, (_, _, constrs)) => fold (fn (_, cargs) => fold (insert op =) (map (length o fst o strip_dtyp) - (List.filter is_rec_type cargs))) constrs) descr []; + (filter is_rec_type cargs))) constrs) descr []; (* interpret construction of datatype *) diff -r 6a72af4e84b8 -r b4534348b8fd src/HOL/Tools/Datatype/datatype_codegen.ML --- a/src/HOL/Tools/Datatype/datatype_codegen.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Thu Oct 29 17:58:26 2009 +0100 @@ -42,8 +42,8 @@ fun add_dt_defs thy defs dep module (descr: Datatype.descr) sorts gr = let - val descr' = List.filter (can (map DatatypeAux.dest_DtTFree o #2 o snd)) descr; - val rtnames = map (#1 o snd) (List.filter (fn (_, (_, _, cs)) => + val descr' = filter (can (map DatatypeAux.dest_DtTFree o #2 o snd)) descr; + val rtnames = map (#1 o snd) (filter (fn (_, (_, _, cs)) => exists (exists DatatypeAux.is_rec_type o snd) cs) descr'); val (_, (tname, _, _)) :: _ = descr'; diff -r 6a72af4e84b8 -r b4534348b8fd src/HOL/Tools/Datatype/datatype_prop.ML --- a/src/HOL/Tools/Datatype/datatype_prop.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML Thu Oct 29 17:58:26 2009 +0100 @@ -130,11 +130,11 @@ (make_pred (body_index dt) U $ app_bnds (Free (s, T)) (length Us))) end; - val recs = List.filter is_rec_type cargs; + val recs = filter is_rec_type cargs; val Ts = map (typ_of_dtyp descr' sorts) cargs; val recTs' = map (typ_of_dtyp descr' sorts) recs; val tnames = Name.variant_list pnames (make_tnames Ts); - val rec_tnames = map fst (List.filter (is_rec_type o snd) (tnames ~~ cargs)); + val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs)); val frees = tnames ~~ Ts; val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs'); @@ -190,7 +190,7 @@ map (fn (_, cargs) => let val Ts = map (typ_of_dtyp descr' sorts) cargs; - val recs = List.filter (is_rec_type o fst) (cargs ~~ Ts); + val recs = filter (is_rec_type o fst) (cargs ~~ Ts); fun mk_argT (dt, T) = binder_types T ---> List.nth (rec_result_Ts, body_index dt); @@ -223,11 +223,11 @@ fun make_primrec T comb_t (cname, cargs) (ts, f::fs) = let - val recs = List.filter is_rec_type cargs; + val recs = filter is_rec_type cargs; val Ts = map (typ_of_dtyp descr' sorts) cargs; val recTs' = map (typ_of_dtyp descr' sorts) recs; val tnames = make_tnames Ts; - val rec_tnames = map fst (List.filter (is_rec_type o snd) (tnames ~~ cargs)); + val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs)); val frees = map Free (tnames ~~ Ts); val frees' = map Free (rec_tnames ~~ recTs'); diff -r 6a72af4e84b8 -r b4534348b8fd src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Oct 29 17:58:26 2009 +0100 @@ -444,7 +444,7 @@ val rec_consts = fold add_term_consts_2 cs' []; val intr_consts = fold add_term_consts_2 intr_ts' []; fun unify (cname, cT) = - let val consts = map snd (List.filter (fn c => fst c = cname) intr_consts) + let val consts = map snd (filter (fn c => fst c = cname) intr_consts) in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end; val (env, _) = fold unify rec_consts (Vartab.empty, i'); val subst = map_types (Envir.norm_type env) @@ -1061,7 +1061,7 @@ fun check_modes_pred options with_generator thy param_vs clauses modes gen_modes (p, ms) = let val rs = case AList.lookup (op =) clauses p of SOME rs => rs | NONE => [] - in (p, List.filter (fn m => case find_index + in (p, filter (fn m => case find_index (is_none o check_mode_clause with_generator thy param_vs modes gen_modes m) rs of ~1 => true | i => (print_failed_mode options thy modes p m rs i; false)) ms) diff -r 6a72af4e84b8 -r b4534348b8fd src/HOL/Tools/TFL/post.ML --- a/src/HOL/Tools/TFL/post.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/HOL/Tools/TFL/post.ML Thu Oct 29 17:58:26 2009 +0100 @@ -71,7 +71,7 @@ | _ => r RS P_imp_P_eq_True (*Is this the best way to invoke the simplifier??*) -fun rewrite L = rewrite_rule (map mk_meta_eq (List.filter(not o id_thm) L)) +fun rewrite L = rewrite_rule (map mk_meta_eq (filter_out id_thm L)) fun join_assums th = let val thy = Thm.theory_of_thm th diff -r 6a72af4e84b8 -r b4534348b8fd src/HOL/Tools/TFL/rules.ML --- a/src/HOL/Tools/TFL/rules.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/HOL/Tools/TFL/rules.ML Thu Oct 29 17:58:26 2009 +0100 @@ -807,7 +807,7 @@ (prover names) (ss0 addsimps [cut_lemma'] addeqcongs congs) ctm val th2 = equal_elim th1 th in - (th2, List.filter (not o restricted) (!tc_list)) + (th2, filter_out restricted (!tc_list)) end; diff -r 6a72af4e84b8 -r b4534348b8fd src/HOL/Tools/TFL/tfl.ML --- a/src/HOL/Tools/TFL/tfl.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/HOL/Tools/TFL/tfl.ML Thu Oct 29 17:58:26 2009 +0100 @@ -423,13 +423,13 @@ end; -fun givens pats = map pat_of (List.filter given pats); +fun givens pats = map pat_of (filter given pats); fun post_definition meta_tflCongs (theory, (def, pats)) = let val tych = Thry.typecheck theory val f = #lhs(S.dest_eq(concl def)) val corollary = R.MATCH_MP Thms.WFREC_COROLLARY def - val pats' = List.filter given pats + val pats' = filter given pats val given_pats = map pat_of pats' val rows = map row_of_pat pats' val WFR = #ant(S.dest_imp(concl corollary)) @@ -821,7 +821,7 @@ let val ex_tm = S.mk_exists{Bvar=v,Body=tm} in (ex_tm, R.CHOOSE(tych v, R.ASSUME (tych ex_tm)) thm) end - val [veq] = List.filter (can S.dest_eq) (#1 (R.dest_thm thm)) + val [veq] = filter (can S.dest_eq) (#1 (R.dest_thm thm)) val {lhs,rhs} = S.dest_eq veq val L = S.free_vars_lr rhs in #2 (fold_rev CHOOSER L (veq,thm)) end; diff -r 6a72af4e84b8 -r b4534348b8fd src/HOL/Tools/choice_specification.ML --- a/src/HOL/Tools/choice_specification.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/HOL/Tools/choice_specification.ML Thu Oct 29 17:58:26 2009 +0100 @@ -143,7 +143,7 @@ val (_, c') = Type.varify [] c val (cname,ctyp) = dest_Const c' in - case List.filter (fn t => let val (name,typ) = dest_Const t + case filter (fn t => let val (name,typ) = dest_Const t in name = cname andalso Sign.typ_equiv thy (typ, ctyp) end) thawed_prop_consts of [] => error ("Specification: No suitable instances of constant \"" ^ Syntax.string_of_term_global thy c ^ "\" found") diff -r 6a72af4e84b8 -r b4534348b8fd src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/HOL/Tools/inductive.ML Thu Oct 29 17:58:26 2009 +0100 @@ -392,7 +392,7 @@ list_all (params', Logic.list_implies (map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (frees ~~ us) @ ts, P)); - val c_intrs = (List.filter (equal c o #1 o #1 o #1) intrs); + val c_intrs = filter (equal c o #1 o #1 o #1) intrs; val prems = HOLogic.mk_Trueprop (list_comb (c, params @ frees)) :: map mk_elim_prem (map #1 c_intrs) in diff -r 6a72af4e84b8 -r b4534348b8fd src/HOL/Tools/inductive_codegen.ML --- a/src/HOL/Tools/inductive_codegen.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/HOL/Tools/inductive_codegen.ML Thu Oct 29 17:58:26 2009 +0100 @@ -174,7 +174,7 @@ let val is' = map (fn i => i - k) (List.drop (is, k)) in map (fn x => Mode (m, is', x)) (cprods (map (fn (NONE, _) => [NONE] - | (SOME js, arg) => map SOME (List.filter + | (SOME js, arg) => map SOME (filter (fn Mode (_, js', _) => js=js') (modes_of modes arg))) (iss ~~ args1))) end @@ -237,7 +237,7 @@ fun check_modes_pred thy arg_vs preds modes (p, ms) = let val SOME rs = AList.lookup (op =) preds p - in (p, List.filter (fn m => case find_index + in (p, filter (fn m => case find_index (not o check_mode_clause thy arg_vs modes m) rs of ~1 => true | i => (message ("Clause " ^ string_of_int (i+1) ^ " of " ^ diff -r 6a72af4e84b8 -r b4534348b8fd src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/HOL/Tools/lin_arith.ML Thu Oct 29 17:58:26 2009 +0100 @@ -681,7 +681,7 @@ val beta_eta_norm = map (apsnd (map (Envir.eta_contract o Envir.beta_norm))) split_goals (* TRY (etac notE) THEN eq_assume_tac: *) - val result = List.filter (not o negated_term_occurs_positively o snd) + val result = filter_out (negated_term_occurs_positively o snd) beta_eta_norm in result diff -r 6a72af4e84b8 -r b4534348b8fd src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/HOL/Tools/meson.ML Thu Oct 29 17:58:26 2009 +0100 @@ -450,7 +450,7 @@ (*Is the given disjunction an all-negative support clause?*) fun is_negative th = forall (not o #1) (literals (prop_of th)); -val neg_clauses = List.filter is_negative; +val neg_clauses = filter is_negative; (***** MESON PROOF PROCEDURE *****) diff -r 6a72af4e84b8 -r b4534348b8fd src/HOL/Tools/metis_tools.ML --- a/src/HOL/Tools/metis_tools.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/HOL/Tools/metis_tools.ML Thu Oct 29 17:58:26 2009 +0100 @@ -680,7 +680,7 @@ val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode) val _ = trace_msg (fn () => "START METIS PROVE PROCESS") in - case List.filter (is_false o prop_of) cls of + case filter (is_false o prop_of) cls of false_th::_ => [false_th RS @{thm FalseE}] | [] => case refute thms of diff -r 6a72af4e84b8 -r b4534348b8fd src/HOL/Tools/old_primrec.ML --- a/src/HOL/Tools/old_primrec.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/HOL/Tools/old_primrec.ML Thu Oct 29 17:58:26 2009 +0100 @@ -195,7 +195,7 @@ NONE => let val dummy_fns = map (fn (_, cargs) => Const ("HOL.undefined", - replicate ((length cargs) + (length (List.filter is_rec_type cargs))) + replicate (length cargs + length (filter is_rec_type cargs)) dummyT ---> HOLogic.unitT)) constrs; val _ = warning ("No function definition for datatype " ^ quote tname) in diff -r 6a72af4e84b8 -r b4534348b8fd src/HOL/Tools/primrec.ML --- a/src/HOL/Tools/primrec.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/HOL/Tools/primrec.ML Thu Oct 29 17:58:26 2009 +0100 @@ -178,7 +178,7 @@ NONE => let val dummy_fns = map (fn (_, cargs) => Const ("HOL.undefined", - replicate ((length cargs) + (length (List.filter is_rec_type cargs))) + replicate (length cargs + length (filter is_rec_type cargs)) dummyT ---> HOLogic.unitT)) constrs; val _ = warning ("No function definition for datatype " ^ quote tname) in diff -r 6a72af4e84b8 -r b4534348b8fd src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/HOL/Tools/refute.ML Thu Oct 29 17:58:26 2009 +0100 @@ -394,7 +394,7 @@ (* (string * int) list *) val sizes = map_filter (fn (name, value) => Option.map (pair name) (Int.fromString value)) - (List.filter (fn (name, _) => name<>"minsize" andalso name<>"maxsize" + (filter (fn (name, _) => name<>"minsize" andalso name<>"maxsize" andalso name<>"maxvars" andalso name<>"maxtime" andalso name<>"satsolver") allparams) in @@ -1070,8 +1070,7 @@ (* continue search *) next max (len+1) (sum+x1) (x2::xs) (* only consider those types for which the size is not fixed *) - val mutables = List.filter - (not o (AList.defined (op =) sizes) o string_of_typ o fst) xs + val mutables = filter_out (AList.defined (op =) sizes o string_of_typ o fst) xs (* subtract 'minsize' from every size (will be added again at the end) *) val diffs = map (fn (_, n) => n-minsize) mutables in @@ -2552,7 +2551,7 @@ (* arguments *) val (_, _, constrs) = the (AList.lookup (op =) descr idx) val (_, dtyps) = List.nth (constrs, c) - val rec_dtyps_args = List.filter + val rec_dtyps_args = filter (DatatypeAux.is_rec_type o fst) (dtyps ~~ args) (* map those indices to interpretations *) val rec_dtyps_intrs = map (fn (dtyp, arg) => diff -r 6a72af4e84b8 -r b4534348b8fd src/HOL/Tools/sat_solver.ML --- a/src/HOL/Tools/sat_solver.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/HOL/Tools/sat_solver.ML Thu Oct 29 17:58:26 2009 +0100 @@ -272,7 +272,7 @@ else parse_lines lines in - (parse_lines o (List.filter (fn l => l <> "")) o split_lines o File.read) path + (parse_lines o filter (fn l => l <> "") o split_lines o File.read) path end; (* ------------------------------------------------------------------------- *) @@ -352,7 +352,7 @@ o (map int_from_string) o (maps (String.fields (fn c => c mem [#" ", #"\t", #"\n"]))) o filter_preamble - o (List.filter (fn l => l <> "")) + o filter (fn l => l <> "") o split_lines o File.read) path diff -r 6a72af4e84b8 -r b4534348b8fd src/HOL/ex/predicate_compile.ML --- a/src/HOL/ex/predicate_compile.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/HOL/ex/predicate_compile.ML Thu Oct 29 17:58:26 2009 +0100 @@ -999,7 +999,7 @@ fun check_modes_pred with_generator thy param_vs preds modes gen_modes (p, ms) = let val SOME rs = AList.lookup (op =) preds p - in (p, List.filter (fn m => case find_index + in (p, filter (fn m => case find_index (is_none o check_mode_clause with_generator thy param_vs modes gen_modes m) rs of ~1 => true | i => (tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^ diff -r 6a72af4e84b8 -r b4534348b8fd src/HOLCF/Tools/Domain/domain_axioms.ML --- a/src/HOLCF/Tools/Domain/domain_axioms.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Thu Oct 29 17:58:26 2009 +0100 @@ -184,7 +184,7 @@ fun one_con (con,args) = let val nonrec_args = filter_out is_rec args; - val rec_args = List.filter is_rec args; + val rec_args = filter is_rec args; val recs_cnt = length rec_args; val allargs = nonrec_args @ rec_args @ map (upd_vname (fn s=> s^"'")) rec_args; diff -r 6a72af4e84b8 -r b4534348b8fd src/HOLCF/Tools/Domain/domain_library.ML --- a/src/HOLCF/Tools/Domain/domain_library.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/HOLCF/Tools/Domain/domain_library.ML Thu Oct 29 17:58:26 2009 +0100 @@ -241,8 +241,8 @@ val upd_vname = upd_third; fun is_rec arg = rec_of arg >=0; fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg); -fun nonlazy args = map vname (filter_out is_lazy args); -fun nonlazy_rec args = map vname (List.filter is_nonlazy_rec args); +fun nonlazy args = map vname (filter_out is_lazy args); +fun nonlazy_rec args = map vname (filter is_nonlazy_rec args); (* ----- combinators for making dtyps ----- *) diff -r 6a72af4e84b8 -r b4534348b8fd src/HOLCF/Tools/Domain/domain_theorems.ML --- a/src/HOLCF/Tools/Domain/domain_theorems.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Thu Oct 29 17:58:26 2009 +0100 @@ -446,7 +446,7 @@ val nlas = nonlazy args; val vns = map vname args; val vnn = List.nth (vns, n); - val nlas' = List.filter (fn v => v <> vnn) nlas; + val nlas' = filter (fn v => v <> vnn) nlas; val lhs = (%%:sel)`(con_app con args); val goal = lift_defined %: (nlas', mk_trp (lhs === %:vnn)); fun tacs1 ctxt = @@ -555,7 +555,7 @@ val sargs = case largs of [_] => [] | _ => nonlazy args; val prop = lift_defined %: (sargs, mk_trp (prem === concl)); in pg con_appls prop end; - val cons' = List.filter (fn (_,args) => args<>[]) cons; + val cons' = filter (fn (_,args) => args<>[]) cons; in val _ = trace " Proving inverts..."; val inverts = @@ -593,7 +593,7 @@ else (%# arg); val rhs = con_app2 con one_rhs args; val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs)); - val args' = List.filter (fn a => not (is_rec a orelse is_lazy a)) args; + val args' = filter_out (fn a => is_rec a orelse is_lazy a) args; val stricts = abs_strict :: rep_strict :: @{thms domain_fun_stricts}; fun tacs1 ctxt = map (case_UU_tac ctxt stricts 1 o vname) args'; val rules = [ax_abs_iso] @ @{thms domain_fun_simps}; @@ -616,7 +616,7 @@ fun has_nonlazy_rec (_, args) = exists is_nonlazy_rec args; in val _ = trace " Proving copy_stricts..."; - val copy_stricts = map one_strict (List.filter has_nonlazy_rec cons); + val copy_stricts = map one_strict (filter has_nonlazy_rec cons); end; val copy_rews = copy_strict :: copy_apps @ copy_stricts; @@ -722,7 +722,7 @@ in Library.foldr mk_all (map vname args, lhs === rhs) end; fun mk_eqns ((dn, _), cons) = map (mk_eqn dn) cons; val goal = mk_trp (foldr1 mk_conj (maps mk_eqns eqs)); - val simps = List.filter (has_fewer_prems 1) copy_rews; + val simps = filter (has_fewer_prems 1) copy_rews; fun con_tac ctxt (con, args) = if nonlazy_rec args = [] then all_tac @@ -747,7 +747,7 @@ let fun ind_hyp arg = %:(P_name (1 + rec_of arg)) $ bound_arg args arg; val t1 = mk_trp (%:p $ con_app2 con (bound_arg args) args); - val t2 = lift ind_hyp (List.filter is_rec args, t1); + val t2 = lift ind_hyp (filter is_rec args, t1); val t3 = lift_defined (bound_arg (map vname args)) (nonlazy args, t2); in Library.foldr mk_All (map vname args, t3) end; @@ -767,7 +767,7 @@ maps (fn (_,args) => resolve_tac prems 1 :: map (K(atac 1)) (nonlazy args) @ - map (K(atac 1)) (List.filter is_rec args)) + map (K(atac 1)) (filter is_rec args)) cons)) conss); local @@ -812,10 +812,10 @@ (List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg); fun con_tacs (con, args) = asm_simp_tac take_ss 1 :: - map arg_tac (List.filter is_nonlazy_rec args) @ + map arg_tac (filter is_nonlazy_rec args) @ [resolve_tac prems 1] @ - map (K (atac 1)) (nonlazy args) @ - map (K (etac spec 1)) (List.filter is_rec args); + map (K (atac 1)) (nonlazy args) @ + map (K (etac spec 1)) (filter is_rec args); fun cases_tacs (cons, cases) = res_inst_tac context [(("x", 0), "x")] cases 1 :: asm_simp_tac (take_ss addsimps prems) 1 :: diff -r 6a72af4e84b8 -r b4534348b8fd src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/Provers/Arith/fast_lin_arith.ML Thu Oct 29 17:58:26 2009 +0100 @@ -340,7 +340,7 @@ case ty of Eq => k <> 0 | Le => k > 0 | Lt => k >= 0; fun calc_blowup l = - let val (p,n) = List.partition (curry (op <) 0) (List.filter (curry (op <>) 0) l) + let val (p,n) = List.partition (curry (op <) 0) (filter (curry (op <>) 0) l) in length p * length n end; (* ------------------------------------------------------------------------- *) diff -r 6a72af4e84b8 -r b4534348b8fd src/Provers/classical.ML --- a/src/Provers/classical.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/Provers/classical.ML Thu Oct 29 17:58:26 2009 +0100 @@ -670,7 +670,7 @@ (*version of bimatch_from_nets_tac that only applies rules that create precisely n subgoals.*) fun n_bimatch_from_nets_tac n = - biresolution_from_nets_tac (order_list o List.filter (nsubgoalsP n)) true; + biresolution_from_nets_tac (order_list o filter (nsubgoalsP n)) true; fun eq_contr_tac i = ematch_tac [not_elim] i THEN eq_assume_tac i; val eq_assume_contr_tac = eq_assume_tac ORELSE' eq_contr_tac; diff -r 6a72af4e84b8 -r b4534348b8fd src/Provers/splitter.ML --- a/src/Provers/splitter.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/Provers/splitter.ML Thu Oct 29 17:58:26 2009 +0100 @@ -192,7 +192,7 @@ if n > length ts then [] else let val lev = length apsns val lbnos = fold add_lbnos (Library.take (n, ts)) [] - val flbnos = List.filter (fn i => i < lev) lbnos + val flbnos = filter (fn i => i < lev) lbnos val tt = incr_boundvars (~lev) t in if null flbnos then if T = T' then [(thm,[],pos,TB,tt)] else [] diff -r 6a72af4e84b8 -r b4534348b8fd src/Pure/Isar/rule_insts.ML --- a/src/Pure/Isar/rule_insts.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/Pure/Isar/rule_insts.ML Thu Oct 29 17:58:26 2009 +0100 @@ -268,7 +268,7 @@ (* Separate type and term insts *) fun has_type_var ((x, _), _) = (case Symbol.explode x of "'" :: _ => true | _ => false); - val Tinsts = List.filter has_type_var insts; + val Tinsts = filter has_type_var insts; val tinsts = filter_out has_type_var insts; (* Tactic *) diff -r 6a72af4e84b8 -r b4534348b8fd src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/Pure/Proof/extraction.ML Thu Oct 29 17:58:26 2009 +0100 @@ -651,7 +651,7 @@ val nt = Envir.beta_norm t; val args = filter_out (fn v => member (op =) rtypes (tname_of (body_type (fastype_of v)))) (vfs_of prop); - val args' = List.filter (fn v => Logic.occs (v, nt)) args; + val args' = filter (fn v => Logic.occs (v, nt)) args; val t' = mkabs nt args'; val T = fastype_of t'; val cname = extr_name s vs'; diff -r 6a72af4e84b8 -r b4534348b8fd src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/Pure/Syntax/parser.ML Thu Oct 29 17:58:26 2009 +0100 @@ -615,11 +615,11 @@ (*Get all rhss with precedence >= minPrec*) -fun getRHS minPrec = List.filter (fn (_, _, prec:int) => prec >= minPrec); +fun getRHS minPrec = filter (fn (_, _, prec:int) => prec >= minPrec); (*Get all rhss with precedence >= minPrec and < maxPrec*) fun getRHS' minPrec maxPrec = - List.filter (fn (_, _, prec:int) => prec >= minPrec andalso prec < maxPrec); + filter (fn (_, _, prec:int) => prec >= minPrec andalso prec < maxPrec); (*Make states using a list of rhss*) fun mkStates i minPrec lhsID rhss = @@ -655,19 +655,19 @@ in update (used, []) end; fun getS A maxPrec Si = - List.filter + filter (fn (_, _, _, Nonterminal (B, prec) :: _, _, _) => A = B andalso prec <= maxPrec | _ => false) Si; fun getS' A maxPrec minPrec Si = - List.filter + filter (fn (_, _, _, Nonterminal (B, prec) :: _, _, _) => A = B andalso prec > minPrec andalso prec <= maxPrec | _ => false) Si; fun getStates Estate i ii A maxPrec = - List.filter + filter (fn (_, _, _, Nonterminal (B, prec) :: _, _, _) => A = B andalso prec <= maxPrec | _ => false) diff -r 6a72af4e84b8 -r b4534348b8fd src/Pure/Syntax/syn_ext.ML --- a/src/Pure/Syntax/syn_ext.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/Pure/Syntax/syn_ext.ML Thu Oct 29 17:58:26 2009 +0100 @@ -218,7 +218,7 @@ val read_symbs = map_filter I o the o Scan.read Symbol.stopper scan_symbs; fun unique_index xsymbs = - if length (List.filter is_index xsymbs) <= 1 then xsymbs + if length (filter is_index xsymbs) <= 1 then xsymbs else error "Duplicate index arguments (\\)"; in @@ -226,7 +226,7 @@ val read_mfix = unique_index o read_symbs o Symbol.explode; fun mfix_delims sy = fold_rev (fn Delim s => cons s | _ => I) (read_mfix sy) []; -val mfix_args = length o List.filter is_argument o read_mfix; +val mfix_args = length o filter is_argument o read_mfix; val escape_mfix = implode o map (fn s => if is_meta s then "'" ^ s else s) o Symbol.explode; @@ -276,7 +276,7 @@ val raw_symbs = read_mfix sy handle ERROR msg => err_in_mfix msg mfix; - val args = List.filter (fn Argument _ => true | _ => false) raw_symbs; + val args = filter (fn Argument _ => true | _ => false) raw_symbs; val (const', typ', parse_rules) = if not (exists is_index args) then (const, typ, []) else @@ -312,7 +312,7 @@ val xprod' = if Lexicon.is_terminal lhs' then err_in_mfix ("Illegal lhs: " ^ lhs') mfix else if const <> "" then xprod - else if length (List.filter is_argument symbs') <> 1 then + else if length (filter is_argument symbs') <> 1 then err_in_mfix "Copy production must have exactly one argument" mfix else if exists is_terminal symbs' then xprod else XProd (lhs', map rem_pri symbs', "", chain_pri); diff -r 6a72af4e84b8 -r b4534348b8fd src/Pure/codegen.ML --- a/src/Pure/codegen.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/Pure/codegen.ML Thu Oct 29 17:58:26 2009 +0100 @@ -137,7 +137,7 @@ | args_of (Ignore :: ms) (_ :: xs) = args_of ms xs | args_of (_ :: ms) xs = args_of ms xs; -fun num_args_of x = length (List.filter is_arg x); +fun num_args_of x = length (filter is_arg x); (**** theory data ****) diff -r 6a72af4e84b8 -r b4534348b8fd src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/Pure/proofterm.ML Thu Oct 29 17:58:26 2009 +0100 @@ -1024,7 +1024,7 @@ (** see pattern.ML **) -fun flt (i: int) = List.filter (fn n => n < i); +fun flt (i: int) = filter (fn n => n < i); fun fomatch Ts tymatch j = let diff -r 6a72af4e84b8 -r b4534348b8fd src/Pure/unify.ML --- a/src/Pure/unify.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/Pure/unify.ML Thu Oct 29 17:58:26 2009 +0100 @@ -473,7 +473,7 @@ if i j < i-lev) banned)) + else Bound (i - length (filter (fn j => j < i-lev) banned)) | change lev (Abs (a,T,t)) = Abs (a, T, change(lev+1) t) | change lev (t$u) = change lev t $ change lev u | change lev t = t diff -r 6a72af4e84b8 -r b4534348b8fd src/Tools/IsaPlanner/rw_inst.ML --- a/src/Tools/IsaPlanner/rw_inst.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/Tools/IsaPlanner/rw_inst.ML Thu Oct 29 17:58:26 2009 +0100 @@ -169,7 +169,7 @@ OldTerm.add_term_tfrees (t,tfrees))) ([],[]) ts; val unfixed_tvars = - List.filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars; + filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars; val (fixtyinsts, _) = List.foldr new_tfree ([], map fst tfrees) unfixed_tvars in (fixtyinsts, tfrees) end; diff -r 6a72af4e84b8 -r b4534348b8fd src/ZF/arith_data.ML --- a/src/ZF/arith_data.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/ZF/arith_data.ML Thu Oct 29 17:58:26 2009 +0100 @@ -68,7 +68,7 @@ fun prove_conv name tacs ctxt prems (t,u) = if t aconv u then NONE else - let val prems' = List.filter (not o is_eq_thm) prems + let val prems' = filter_out is_eq_thm prems val goal = Logic.list_implies (map (#prop o Thm.rep_thm) prems', FOLogic.mk_Trueprop (mk_eq_iff (t, u))); in SOME (prems' MRS Goal.prove ctxt [] [] goal (K (EVERY tacs))) diff -r 6a72af4e84b8 -r b4534348b8fd src/ZF/ind_syntax.ML --- a/src/ZF/ind_syntax.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/ZF/ind_syntax.ML Thu Oct 29 17:58:26 2009 +0100 @@ -96,8 +96,8 @@ fun union_params (rec_tm, cs) = let val (_,args) = strip_comb rec_tm fun is_ind arg = (type_of arg = iT) - in case List.filter is_ind (args @ cs) of - [] => @{const 0} + in case filter is_ind (args @ cs) of + [] => @{const 0} | u_args => Balanced_Tree.make mk_Un u_args end;