--- 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
--- 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;
--- 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
--- 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 =
--- 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);
--- 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
--- 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
--- 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 *)
--- 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';
--- 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');
--- 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)
--- 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
--- 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;
--- 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;
--- 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")
--- 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
--- 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 " ^
--- 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
--- 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 *****)
--- 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
--- 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
--- 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
--- 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) =>
--- 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
--- 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 " ^
--- 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;
--- 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 ----- *)
--- 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 ::
--- 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;
(* ------------------------------------------------------------------------- *)
--- 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;
--- 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 []
--- 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 *)
--- 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';
--- 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)
--- 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 (\\<index>)";
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);
--- 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 ****)
--- 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
--- 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<lev then Bound i
else if member (op =) banned (i-lev)
then raise CHANGE_FAIL (**flexible occurrence: give up**)
- else Bound (i - length (List.filter (fn j => 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
--- 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;
--- 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)))
--- 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;