standardized filter/filter_out;
authorwenzelm
Thu Oct 29 17:58:26 2009 +0100 (2009-10-29)
changeset 33317b4534348b8fd
parent 33316 6a72af4e84b8
child 33333 78faaec3209f
standardized filter/filter_out;
src/CCL/Wfd.thy
src/FOLP/simp.ML
src/HOL/Import/import_syntax.ML
src/HOL/Import/shuffler.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_primrec.ML
src/HOL/Tools/Datatype/datatype_abs_proofs.ML
src/HOL/Tools/Datatype/datatype_aux.ML
src/HOL/Tools/Datatype/datatype_codegen.ML
src/HOL/Tools/Datatype/datatype_prop.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/TFL/post.ML
src/HOL/Tools/TFL/rules.ML
src/HOL/Tools/TFL/tfl.ML
src/HOL/Tools/choice_specification.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/metis_tools.ML
src/HOL/Tools/old_primrec.ML
src/HOL/Tools/primrec.ML
src/HOL/Tools/refute.ML
src/HOL/Tools/sat_solver.ML
src/HOL/ex/predicate_compile.ML
src/HOLCF/Tools/Domain/domain_axioms.ML
src/HOLCF/Tools/Domain/domain_library.ML
src/HOLCF/Tools/Domain/domain_theorems.ML
src/Provers/Arith/fast_lin_arith.ML
src/Provers/classical.ML
src/Provers/splitter.ML
src/Pure/Isar/rule_insts.ML
src/Pure/Proof/extraction.ML
src/Pure/Syntax/parser.ML
src/Pure/Syntax/syn_ext.ML
src/Pure/codegen.ML
src/Pure/proofterm.ML
src/Pure/unify.ML
src/Tools/IsaPlanner/rw_inst.ML
src/ZF/arith_data.ML
src/ZF/ind_syntax.ML
     1.1 --- a/src/CCL/Wfd.thy	Thu Oct 29 16:59:12 2009 +0100
     1.2 +++ b/src/CCL/Wfd.thy	Thu Oct 29 17:58:26 2009 +0100
     1.3 @@ -440,7 +440,7 @@
     1.4  
     1.5  fun IHinst tac rls = SUBGOAL (fn (Bi,i) =>
     1.6    let val bvs = bvars Bi []
     1.7 -      val ihs = List.filter could_IH (Logic.strip_assums_hyp Bi)
     1.8 +      val ihs = filter could_IH (Logic.strip_assums_hyp Bi)
     1.9        val rnames = map (fn x=>
    1.10                      let val (a,b) = get_bno [] 0 x
    1.11                      in (List.nth(bvs,a),b) end) ihs
     2.1 --- a/src/FOLP/simp.ML	Thu Oct 29 16:59:12 2009 +0100
     2.2 +++ b/src/FOLP/simp.ML	Thu Oct 29 17:58:26 2009 +0100
     2.3 @@ -215,7 +215,7 @@
     2.4  
     2.5  fun add_norm_tags congs =
     2.6      let val ccs = map cong_const congs
     2.7 -        val new_asms = List.filter (exists not o #2)
     2.8 +        val new_asms = filter (exists not o #2)
     2.9                  (ccs ~~ (map (map atomic o prems_of) congs));
    2.10      in add_norms(congs,ccs,new_asms) end;
    2.11  
     3.1 --- a/src/HOL/Import/import_syntax.ML	Thu Oct 29 16:59:12 2009 +0100
     3.2 +++ b/src/HOL/Import/import_syntax.ML	Thu Oct 29 17:58:26 2009 +0100
     3.3 @@ -61,7 +61,7 @@
     3.4                  val thyname = get_generating_thy thy
     3.5                  val segname = get_import_segment thy
     3.6                  val (int_thms,facts) = Replay.setup_int_thms thyname thy
     3.7 -                val thmnames = List.filter (not o should_ignore thyname thy) facts
     3.8 +                val thmnames = filter_out (should_ignore thyname thy) facts
     3.9                  fun replay thy = 
    3.10                      let
    3.11                          val _ = ImportRecorder.load_history thyname
     4.1 --- a/src/HOL/Import/shuffler.ML	Thu Oct 29 16:59:12 2009 +0100
     4.2 +++ b/src/HOL/Import/shuffler.ML	Thu Oct 29 17:58:26 2009 +0100
     4.3 @@ -628,7 +628,7 @@
     4.4          val all_thms =
     4.5            map (`Thm.get_name_hint) (maps #2 (Facts.dest_static [] (PureThy.facts_of thy)))
     4.6      in
     4.7 -        List.filter (match_consts ignored t) all_thms
     4.8 +        filter (match_consts ignored t) all_thms
     4.9      end
    4.10  
    4.11  fun gen_shuffle_tac ctxt search thms i st =
     5.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Thu Oct 29 16:59:12 2009 +0100
     5.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Thu Oct 29 17:58:26 2009 +0100
     5.3 @@ -66,7 +66,7 @@
     5.4  
     5.5  fun mk_case_names_exhausts descr new =
     5.6    map (RuleCases.case_names o exhaust_cases descr o #1)
     5.7 -    (List.filter (fn ((_, (name, _, _))) => name mem_string new) descr);
     5.8 +    (filter (fn ((_, (name, _, _))) => name mem_string new) descr);
     5.9  
    5.10  end;
    5.11  
    5.12 @@ -1166,11 +1166,11 @@
    5.13  
    5.14      fun make_ind_prem fsT f k T ((cname, cargs), idxs) =
    5.15        let
    5.16 -        val recs = List.filter is_rec_type cargs;
    5.17 +        val recs = filter is_rec_type cargs;
    5.18          val Ts = map (typ_of_dtyp descr'' sorts) cargs;
    5.19          val recTs' = map (typ_of_dtyp descr'' sorts) recs;
    5.20          val tnames = Name.variant_list pnames (DatatypeProp.make_tnames Ts);
    5.21 -        val rec_tnames = map fst (List.filter (is_rec_type o snd) (tnames ~~ cargs));
    5.22 +        val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
    5.23          val frees = tnames ~~ Ts;
    5.24          val frees' = partition_cargs idxs frees;
    5.25          val z = (Name.variant tnames "z", fsT);
     6.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Thu Oct 29 16:59:12 2009 +0100
     6.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Thu Oct 29 17:58:26 2009 +0100
     6.3 @@ -193,7 +193,7 @@
     6.4       NONE =>
     6.5         let
     6.6           val dummy_fns = map (fn (_, cargs) => Const (@{const_name undefined},
     6.7 -           replicate ((length cargs) + (length (List.filter is_rec_type cargs)))
     6.8 +           replicate (length cargs + length (filter is_rec_type cargs))
     6.9               dummyT ---> HOLogic.unitT)) constrs;
    6.10           val _ = warning ("No function definition for datatype " ^ quote tname)
    6.11         in
     7.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Oct 29 16:59:12 2009 +0100
     7.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Oct 29 17:58:26 2009 +0100
     7.3 @@ -292,7 +292,7 @@
     7.4      val case_dummy_fns = map (fn (_, (_, _, constrs)) => map (fn (_, cargs) =>
     7.5        let
     7.6          val Ts = map (typ_of_dtyp descr' sorts) cargs;
     7.7 -        val Ts' = map mk_dummyT (List.filter is_rec_type cargs)
     7.8 +        val Ts' = map mk_dummyT (filter is_rec_type cargs)
     7.9        in Const (@{const_name undefined}, Ts @ Ts' ---> T')
    7.10        end) constrs) descr';
    7.11  
    7.12 @@ -305,7 +305,7 @@
    7.13            val (fns1, fns2) = split_list (map (fn ((_, cargs), j) =>
    7.14              let
    7.15                val Ts = map (typ_of_dtyp descr' sorts) cargs;
    7.16 -              val Ts' = Ts @ map mk_dummyT (List.filter is_rec_type cargs);
    7.17 +              val Ts' = Ts @ map mk_dummyT (filter is_rec_type cargs);
    7.18                val frees' = map (uncurry (mk_Free "x")) (Ts' ~~ (1 upto length Ts'));
    7.19                val frees = Library.take (length cargs, frees');
    7.20                val free = mk_Free "f" (Ts ---> T') j
     8.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Thu Oct 29 16:59:12 2009 +0100
     8.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Thu Oct 29 17:58:26 2009 +0100
     8.3 @@ -231,7 +231,7 @@
     8.4  
     8.5  fun name_of_typ (Type (s, Ts)) =
     8.6        let val s' = Long_Name.base_name s
     8.7 -      in space_implode "_" (List.filter (not o equal "") (map name_of_typ Ts) @
     8.8 +      in space_implode "_" (filter_out (equal "") (map name_of_typ Ts) @
     8.9          [if Syntax.is_identifier s' then s' else "x"])
    8.10        end
    8.11    | name_of_typ _ = "";
    8.12 @@ -272,7 +272,7 @@
    8.13  
    8.14  fun get_arities descr = fold (fn (_, (_, _, constrs)) =>
    8.15    fold (fn (_, cargs) => fold (insert op =) (map (length o fst o strip_dtyp)
    8.16 -    (List.filter is_rec_type cargs))) constrs) descr [];
    8.17 +    (filter is_rec_type cargs))) constrs) descr [];
    8.18  
    8.19  (* interpret construction of datatype *)
    8.20  
     9.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Thu Oct 29 16:59:12 2009 +0100
     9.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Thu Oct 29 17:58:26 2009 +0100
     9.3 @@ -42,8 +42,8 @@
     9.4  
     9.5  fun add_dt_defs thy defs dep module (descr: Datatype.descr) sorts gr =
     9.6    let
     9.7 -    val descr' = List.filter (can (map DatatypeAux.dest_DtTFree o #2 o snd)) descr;
     9.8 -    val rtnames = map (#1 o snd) (List.filter (fn (_, (_, _, cs)) =>
     9.9 +    val descr' = filter (can (map DatatypeAux.dest_DtTFree o #2 o snd)) descr;
    9.10 +    val rtnames = map (#1 o snd) (filter (fn (_, (_, _, cs)) =>
    9.11        exists (exists DatatypeAux.is_rec_type o snd) cs) descr');
    9.12  
    9.13      val (_, (tname, _, _)) :: _ = descr';
    10.1 --- a/src/HOL/Tools/Datatype/datatype_prop.ML	Thu Oct 29 16:59:12 2009 +0100
    10.2 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Thu Oct 29 17:58:26 2009 +0100
    10.3 @@ -130,11 +130,11 @@
    10.4              (make_pred (body_index dt) U $ app_bnds (Free (s, T)) (length Us)))
    10.5            end;
    10.6  
    10.7 -        val recs = List.filter is_rec_type cargs;
    10.8 +        val recs = filter is_rec_type cargs;
    10.9          val Ts = map (typ_of_dtyp descr' sorts) cargs;
   10.10          val recTs' = map (typ_of_dtyp descr' sorts) recs;
   10.11          val tnames = Name.variant_list pnames (make_tnames Ts);
   10.12 -        val rec_tnames = map fst (List.filter (is_rec_type o snd) (tnames ~~ cargs));
   10.13 +        val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
   10.14          val frees = tnames ~~ Ts;
   10.15          val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs');
   10.16  
   10.17 @@ -190,7 +190,7 @@
   10.18        map (fn (_, cargs) =>
   10.19          let
   10.20            val Ts = map (typ_of_dtyp descr' sorts) cargs;
   10.21 -          val recs = List.filter (is_rec_type o fst) (cargs ~~ Ts);
   10.22 +          val recs = filter (is_rec_type o fst) (cargs ~~ Ts);
   10.23  
   10.24            fun mk_argT (dt, T) =
   10.25              binder_types T ---> List.nth (rec_result_Ts, body_index dt);
   10.26 @@ -223,11 +223,11 @@
   10.27  
   10.28      fun make_primrec T comb_t (cname, cargs) (ts, f::fs) =
   10.29        let
   10.30 -        val recs = List.filter is_rec_type cargs;
   10.31 +        val recs = filter is_rec_type cargs;
   10.32          val Ts = map (typ_of_dtyp descr' sorts) cargs;
   10.33          val recTs' = map (typ_of_dtyp descr' sorts) recs;
   10.34          val tnames = make_tnames Ts;
   10.35 -        val rec_tnames = map fst (List.filter (is_rec_type o snd) (tnames ~~ cargs));
   10.36 +        val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
   10.37          val frees = map Free (tnames ~~ Ts);
   10.38          val frees' = map Free (rec_tnames ~~ recTs');
   10.39  
    11.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Oct 29 16:59:12 2009 +0100
    11.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Oct 29 17:58:26 2009 +0100
    11.3 @@ -444,7 +444,7 @@
    11.4       val rec_consts = fold add_term_consts_2 cs' [];
    11.5       val intr_consts = fold add_term_consts_2 intr_ts' [];
    11.6       fun unify (cname, cT) =
    11.7 -       let val consts = map snd (List.filter (fn c => fst c = cname) intr_consts)
    11.8 +       let val consts = map snd (filter (fn c => fst c = cname) intr_consts)
    11.9         in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end;
   11.10       val (env, _) = fold unify rec_consts (Vartab.empty, i');
   11.11       val subst = map_types (Envir.norm_type env)
   11.12 @@ -1061,7 +1061,7 @@
   11.13  fun check_modes_pred options with_generator thy param_vs clauses modes gen_modes (p, ms) =
   11.14    let
   11.15      val rs = case AList.lookup (op =) clauses p of SOME rs => rs | NONE => []
   11.16 -  in (p, List.filter (fn m => case find_index
   11.17 +  in (p, filter (fn m => case find_index
   11.18      (is_none o check_mode_clause with_generator thy param_vs modes gen_modes m) rs of
   11.19        ~1 => true
   11.20      | i => (print_failed_mode options thy modes p m rs i; false)) ms)
    12.1 --- a/src/HOL/Tools/TFL/post.ML	Thu Oct 29 16:59:12 2009 +0100
    12.2 +++ b/src/HOL/Tools/TFL/post.ML	Thu Oct 29 17:58:26 2009 +0100
    12.3 @@ -71,7 +71,7 @@
    12.4    |   _ => r RS P_imp_P_eq_True
    12.5  
    12.6  (*Is this the best way to invoke the simplifier??*)
    12.7 -fun rewrite L = rewrite_rule (map mk_meta_eq (List.filter(not o id_thm) L))
    12.8 +fun rewrite L = rewrite_rule (map mk_meta_eq (filter_out id_thm L))
    12.9  
   12.10  fun join_assums th =
   12.11    let val thy = Thm.theory_of_thm th
    13.1 --- a/src/HOL/Tools/TFL/rules.ML	Thu Oct 29 16:59:12 2009 +0100
    13.2 +++ b/src/HOL/Tools/TFL/rules.ML	Thu Oct 29 17:58:26 2009 +0100
    13.3 @@ -807,7 +807,7 @@
    13.4        (prover names) (ss0 addsimps [cut_lemma'] addeqcongs congs) ctm
    13.5      val th2 = equal_elim th1 th
    13.6   in
    13.7 - (th2, List.filter (not o restricted) (!tc_list))
    13.8 + (th2, filter_out restricted (!tc_list))
    13.9   end;
   13.10  
   13.11  
    14.1 --- a/src/HOL/Tools/TFL/tfl.ML	Thu Oct 29 16:59:12 2009 +0100
    14.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Thu Oct 29 17:58:26 2009 +0100
    14.3 @@ -423,13 +423,13 @@
    14.4  end;
    14.5  
    14.6  
    14.7 -fun givens pats = map pat_of (List.filter given pats);
    14.8 +fun givens pats = map pat_of (filter given pats);
    14.9  
   14.10  fun post_definition meta_tflCongs (theory, (def, pats)) =
   14.11   let val tych = Thry.typecheck theory
   14.12       val f = #lhs(S.dest_eq(concl def))
   14.13       val corollary = R.MATCH_MP Thms.WFREC_COROLLARY def
   14.14 -     val pats' = List.filter given pats
   14.15 +     val pats' = filter given pats
   14.16       val given_pats = map pat_of pats'
   14.17       val rows = map row_of_pat pats'
   14.18       val WFR = #ant(S.dest_imp(concl corollary))
   14.19 @@ -821,7 +821,7 @@
   14.20          let val ex_tm = S.mk_exists{Bvar=v,Body=tm}
   14.21          in (ex_tm, R.CHOOSE(tych v, R.ASSUME (tych ex_tm)) thm)
   14.22          end
   14.23 -      val [veq] = List.filter (can S.dest_eq) (#1 (R.dest_thm thm))
   14.24 +      val [veq] = filter (can S.dest_eq) (#1 (R.dest_thm thm))
   14.25        val {lhs,rhs} = S.dest_eq veq
   14.26        val L = S.free_vars_lr rhs
   14.27    in  #2 (fold_rev CHOOSER L (veq,thm))  end;
    15.1 --- a/src/HOL/Tools/choice_specification.ML	Thu Oct 29 16:59:12 2009 +0100
    15.2 +++ b/src/HOL/Tools/choice_specification.ML	Thu Oct 29 17:58:26 2009 +0100
    15.3 @@ -143,7 +143,7 @@
    15.4                  val (_, c') = Type.varify [] c
    15.5                  val (cname,ctyp) = dest_Const c'
    15.6              in
    15.7 -                case List.filter (fn t => let val (name,typ) = dest_Const t
    15.8 +                case filter (fn t => let val (name,typ) = dest_Const t
    15.9                                       in name = cname andalso Sign.typ_equiv thy (typ, ctyp)
   15.10                                       end) thawed_prop_consts of
   15.11                      [] => error ("Specification: No suitable instances of constant \"" ^ Syntax.string_of_term_global thy c ^ "\" found")
    16.1 --- a/src/HOL/Tools/inductive.ML	Thu Oct 29 16:59:12 2009 +0100
    16.2 +++ b/src/HOL/Tools/inductive.ML	Thu Oct 29 17:58:26 2009 +0100
    16.3 @@ -392,7 +392,7 @@
    16.4            list_all (params',
    16.5              Logic.list_implies (map (HOLogic.mk_Trueprop o HOLogic.mk_eq)
    16.6                (frees ~~ us) @ ts, P));
    16.7 -        val c_intrs = (List.filter (equal c o #1 o #1 o #1) intrs);
    16.8 +        val c_intrs = filter (equal c o #1 o #1 o #1) intrs;
    16.9          val prems = HOLogic.mk_Trueprop (list_comb (c, params @ frees)) ::
   16.10             map mk_elim_prem (map #1 c_intrs)
   16.11        in
    17.1 --- a/src/HOL/Tools/inductive_codegen.ML	Thu Oct 29 16:59:12 2009 +0100
    17.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Thu Oct 29 17:58:26 2009 +0100
    17.3 @@ -174,7 +174,7 @@
    17.4            let val is' = map (fn i => i - k) (List.drop (is, k))
    17.5            in map (fn x => Mode (m, is', x)) (cprods (map
    17.6              (fn (NONE, _) => [NONE]
    17.7 -              | (SOME js, arg) => map SOME (List.filter
    17.8 +              | (SOME js, arg) => map SOME (filter
    17.9                    (fn Mode (_, js', _) => js=js') (modes_of modes arg)))
   17.10                      (iss ~~ args1)))
   17.11            end
   17.12 @@ -237,7 +237,7 @@
   17.13  
   17.14  fun check_modes_pred thy arg_vs preds modes (p, ms) =
   17.15    let val SOME rs = AList.lookup (op =) preds p
   17.16 -  in (p, List.filter (fn m => case find_index
   17.17 +  in (p, filter (fn m => case find_index
   17.18      (not o check_mode_clause thy arg_vs modes m) rs of
   17.19        ~1 => true
   17.20      | i => (message ("Clause " ^ string_of_int (i+1) ^ " of " ^
    18.1 --- a/src/HOL/Tools/lin_arith.ML	Thu Oct 29 16:59:12 2009 +0100
    18.2 +++ b/src/HOL/Tools/lin_arith.ML	Thu Oct 29 17:58:26 2009 +0100
    18.3 @@ -681,7 +681,7 @@
    18.4    val beta_eta_norm  = map (apsnd (map (Envir.eta_contract o Envir.beta_norm)))
    18.5      split_goals
    18.6    (* TRY (etac notE) THEN eq_assume_tac: *)
    18.7 -  val result         = List.filter (not o negated_term_occurs_positively o snd)
    18.8 +  val result         = filter_out (negated_term_occurs_positively o snd)
    18.9      beta_eta_norm
   18.10  in
   18.11    result
    19.1 --- a/src/HOL/Tools/meson.ML	Thu Oct 29 16:59:12 2009 +0100
    19.2 +++ b/src/HOL/Tools/meson.ML	Thu Oct 29 17:58:26 2009 +0100
    19.3 @@ -450,7 +450,7 @@
    19.4  (*Is the given disjunction an all-negative support clause?*)
    19.5  fun is_negative th = forall (not o #1) (literals (prop_of th));
    19.6  
    19.7 -val neg_clauses = List.filter is_negative;
    19.8 +val neg_clauses = filter is_negative;
    19.9  
   19.10  
   19.11  (***** MESON PROOF PROCEDURE *****)
    20.1 --- a/src/HOL/Tools/metis_tools.ML	Thu Oct 29 16:59:12 2009 +0100
    20.2 +++ b/src/HOL/Tools/metis_tools.ML	Thu Oct 29 17:58:26 2009 +0100
    20.3 @@ -680,7 +680,7 @@
    20.4        val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode)
    20.5        val _ = trace_msg (fn () => "START METIS PROVE PROCESS")
    20.6    in
    20.7 -      case List.filter (is_false o prop_of) cls of
    20.8 +      case filter (is_false o prop_of) cls of
    20.9            false_th::_ => [false_th RS @{thm FalseE}]
   20.10          | [] =>
   20.11        case refute thms of
    21.1 --- a/src/HOL/Tools/old_primrec.ML	Thu Oct 29 16:59:12 2009 +0100
    21.2 +++ b/src/HOL/Tools/old_primrec.ML	Thu Oct 29 17:58:26 2009 +0100
    21.3 @@ -195,7 +195,7 @@
    21.4       NONE =>
    21.5         let
    21.6           val dummy_fns = map (fn (_, cargs) => Const ("HOL.undefined",
    21.7 -           replicate ((length cargs) + (length (List.filter is_rec_type cargs)))
    21.8 +           replicate (length cargs + length (filter is_rec_type cargs))
    21.9               dummyT ---> HOLogic.unitT)) constrs;
   21.10           val _ = warning ("No function definition for datatype " ^ quote tname)
   21.11         in
    22.1 --- a/src/HOL/Tools/primrec.ML	Thu Oct 29 16:59:12 2009 +0100
    22.2 +++ b/src/HOL/Tools/primrec.ML	Thu Oct 29 17:58:26 2009 +0100
    22.3 @@ -178,7 +178,7 @@
    22.4       NONE =>
    22.5         let
    22.6           val dummy_fns = map (fn (_, cargs) => Const ("HOL.undefined",
    22.7 -           replicate ((length cargs) + (length (List.filter is_rec_type cargs)))
    22.8 +           replicate (length cargs + length (filter is_rec_type cargs))
    22.9               dummyT ---> HOLogic.unitT)) constrs;
   22.10           val _ = warning ("No function definition for datatype " ^ quote tname)
   22.11         in
    23.1 --- a/src/HOL/Tools/refute.ML	Thu Oct 29 16:59:12 2009 +0100
    23.2 +++ b/src/HOL/Tools/refute.ML	Thu Oct 29 17:58:26 2009 +0100
    23.3 @@ -394,7 +394,7 @@
    23.4      (* (string * int) list *)
    23.5      val sizes     = map_filter
    23.6        (fn (name, value) => Option.map (pair name) (Int.fromString value))
    23.7 -      (List.filter (fn (name, _) => name<>"minsize" andalso name<>"maxsize"
    23.8 +      (filter (fn (name, _) => name<>"minsize" andalso name<>"maxsize"
    23.9          andalso name<>"maxvars" andalso name<>"maxtime"
   23.10          andalso name<>"satsolver") allparams)
   23.11    in
   23.12 @@ -1070,8 +1070,7 @@
   23.13          (* continue search *)
   23.14          next max (len+1) (sum+x1) (x2::xs)
   23.15      (* only consider those types for which the size is not fixed *)
   23.16 -    val mutables = List.filter
   23.17 -      (not o (AList.defined (op =) sizes) o string_of_typ o fst) xs
   23.18 +    val mutables = filter_out (AList.defined (op =) sizes o string_of_typ o fst) xs
   23.19      (* subtract 'minsize' from every size (will be added again at the end) *)
   23.20      val diffs = map (fn (_, n) => n-minsize) mutables
   23.21    in
   23.22 @@ -2552,7 +2551,7 @@
   23.23                          (* arguments                                         *)
   23.24                          val (_, _, constrs) = the (AList.lookup (op =) descr idx)
   23.25                          val (_, dtyps)      = List.nth (constrs, c)
   23.26 -                        val rec_dtyps_args  = List.filter
   23.27 +                        val rec_dtyps_args  = filter
   23.28                            (DatatypeAux.is_rec_type o fst) (dtyps ~~ args)
   23.29                          (* map those indices to interpretations *)
   23.30                          val rec_dtyps_intrs = map (fn (dtyp, arg) =>
    24.1 --- a/src/HOL/Tools/sat_solver.ML	Thu Oct 29 16:59:12 2009 +0100
    24.2 +++ b/src/HOL/Tools/sat_solver.ML	Thu Oct 29 17:58:26 2009 +0100
    24.3 @@ -272,7 +272,7 @@
    24.4        else
    24.5          parse_lines lines
    24.6    in
    24.7 -    (parse_lines o (List.filter (fn l => l <> "")) o split_lines o File.read) path
    24.8 +    (parse_lines o filter (fn l => l <> "") o split_lines o File.read) path
    24.9    end;
   24.10  
   24.11  (* ------------------------------------------------------------------------- *)
   24.12 @@ -352,7 +352,7 @@
   24.13      o (map int_from_string)
   24.14      o (maps (String.fields (fn c => c mem [#" ", #"\t", #"\n"])))
   24.15      o filter_preamble
   24.16 -    o (List.filter (fn l => l <> ""))
   24.17 +    o filter (fn l => l <> "")
   24.18      o split_lines
   24.19      o File.read)
   24.20        path
    25.1 --- a/src/HOL/ex/predicate_compile.ML	Thu Oct 29 16:59:12 2009 +0100
    25.2 +++ b/src/HOL/ex/predicate_compile.ML	Thu Oct 29 17:58:26 2009 +0100
    25.3 @@ -999,7 +999,7 @@
    25.4  
    25.5  fun check_modes_pred with_generator thy param_vs preds modes gen_modes (p, ms) =
    25.6    let val SOME rs = AList.lookup (op =) preds p
    25.7 -  in (p, List.filter (fn m => case find_index
    25.8 +  in (p, filter (fn m => case find_index
    25.9      (is_none o check_mode_clause with_generator thy param_vs modes gen_modes m) rs of
   25.10        ~1 => true
   25.11      | i => (tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^
    26.1 --- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Thu Oct 29 16:59:12 2009 +0100
    26.2 +++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Thu Oct 29 17:58:26 2009 +0100
    26.3 @@ -184,7 +184,7 @@
    26.4  
    26.5        fun one_con (con,args) = let
    26.6          val nonrec_args = filter_out is_rec args;
    26.7 -        val    rec_args = List.filter     is_rec args;
    26.8 +        val    rec_args = filter is_rec args;
    26.9          val    recs_cnt = length rec_args;
   26.10          val allargs     = nonrec_args @ rec_args
   26.11                            @ map (upd_vname (fn s=> s^"'")) rec_args;
    27.1 --- a/src/HOLCF/Tools/Domain/domain_library.ML	Thu Oct 29 16:59:12 2009 +0100
    27.2 +++ b/src/HOLCF/Tools/Domain/domain_library.ML	Thu Oct 29 17:58:26 2009 +0100
    27.3 @@ -241,8 +241,8 @@
    27.4  val upd_vname =   upd_third;
    27.5  fun is_rec         arg = rec_of arg >=0;
    27.6  fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg);
    27.7 -fun nonlazy     args   = map vname (filter_out is_lazy    args);
    27.8 -fun nonlazy_rec args   = map vname (List.filter is_nonlazy_rec args);
    27.9 +fun nonlazy     args   = map vname (filter_out is_lazy args);
   27.10 +fun nonlazy_rec args   = map vname (filter is_nonlazy_rec args);
   27.11  
   27.12  
   27.13  (* ----- combinators for making dtyps ----- *)
    28.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Oct 29 16:59:12 2009 +0100
    28.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Oct 29 17:58:26 2009 +0100
    28.3 @@ -446,7 +446,7 @@
    28.4        val nlas = nonlazy args;
    28.5        val vns = map vname args;
    28.6        val vnn = List.nth (vns, n);
    28.7 -      val nlas' = List.filter (fn v => v <> vnn) nlas;
    28.8 +      val nlas' = filter (fn v => v <> vnn) nlas;
    28.9        val lhs = (%%:sel)`(con_app con args);
   28.10        val goal = lift_defined %: (nlas', mk_trp (lhs === %:vnn));
   28.11        fun tacs1 ctxt =
   28.12 @@ -555,7 +555,7 @@
   28.13        val sargs = case largs of [_] => [] | _ => nonlazy args;
   28.14        val prop = lift_defined %: (sargs, mk_trp (prem === concl));
   28.15      in pg con_appls prop end;
   28.16 -  val cons' = List.filter (fn (_,args) => args<>[]) cons;
   28.17 +  val cons' = filter (fn (_,args) => args<>[]) cons;
   28.18  in
   28.19    val _ = trace " Proving inverts...";
   28.20    val inverts =
   28.21 @@ -593,7 +593,7 @@
   28.22            else (%# arg);
   28.23        val rhs = con_app2 con one_rhs args;
   28.24        val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs));
   28.25 -      val args' = List.filter (fn a => not (is_rec a orelse is_lazy a)) args;
   28.26 +      val args' = filter_out (fn a => is_rec a orelse is_lazy a) args;
   28.27        val stricts = abs_strict :: rep_strict :: @{thms domain_fun_stricts};
   28.28        fun tacs1 ctxt = map (case_UU_tac ctxt stricts 1 o vname) args';
   28.29        val rules = [ax_abs_iso] @ @{thms domain_fun_simps};
   28.30 @@ -616,7 +616,7 @@
   28.31    fun has_nonlazy_rec (_, args) = exists is_nonlazy_rec args;
   28.32  in
   28.33    val _ = trace " Proving copy_stricts...";
   28.34 -  val copy_stricts = map one_strict (List.filter has_nonlazy_rec cons);
   28.35 +  val copy_stricts = map one_strict (filter has_nonlazy_rec cons);
   28.36  end;
   28.37  
   28.38  val copy_rews = copy_strict :: copy_apps @ copy_stricts;
   28.39 @@ -722,7 +722,7 @@
   28.40          in Library.foldr mk_all (map vname args, lhs === rhs) end;
   28.41        fun mk_eqns ((dn, _), cons) = map (mk_eqn dn) cons;
   28.42        val goal = mk_trp (foldr1 mk_conj (maps mk_eqns eqs));
   28.43 -      val simps = List.filter (has_fewer_prems 1) copy_rews;
   28.44 +      val simps = filter (has_fewer_prems 1) copy_rews;
   28.45        fun con_tac ctxt (con, args) =
   28.46          if nonlazy_rec args = []
   28.47          then all_tac
   28.48 @@ -747,7 +747,7 @@
   28.49      let
   28.50        fun ind_hyp arg = %:(P_name (1 + rec_of arg)) $ bound_arg args arg;
   28.51        val t1 = mk_trp (%:p $ con_app2 con (bound_arg args) args);
   28.52 -      val t2 = lift ind_hyp (List.filter is_rec args, t1);
   28.53 +      val t2 = lift ind_hyp (filter is_rec args, t1);
   28.54        val t3 = lift_defined (bound_arg (map vname args)) (nonlazy args, t2);
   28.55      in Library.foldr mk_All (map vname args, t3) end;
   28.56  
   28.57 @@ -767,7 +767,7 @@
   28.58          maps (fn (_,args) => 
   28.59            resolve_tac prems 1 ::
   28.60            map (K(atac 1)) (nonlazy args) @
   28.61 -          map (K(atac 1)) (List.filter is_rec args))
   28.62 +          map (K(atac 1)) (filter is_rec args))
   28.63          cons))
   28.64        conss);
   28.65    local 
   28.66 @@ -812,10 +812,10 @@
   28.67                (List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg);
   28.68            fun con_tacs (con, args) = 
   28.69              asm_simp_tac take_ss 1 ::
   28.70 -            map arg_tac (List.filter is_nonlazy_rec args) @
   28.71 +            map arg_tac (filter is_nonlazy_rec args) @
   28.72              [resolve_tac prems 1] @
   28.73 -            map (K (atac 1))      (nonlazy args) @
   28.74 -            map (K (etac spec 1)) (List.filter is_rec args);
   28.75 +            map (K (atac 1)) (nonlazy args) @
   28.76 +            map (K (etac spec 1)) (filter is_rec args);
   28.77            fun cases_tacs (cons, cases) =
   28.78              res_inst_tac context [(("x", 0), "x")] cases 1 ::
   28.79              asm_simp_tac (take_ss addsimps prems) 1 ::
    29.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Thu Oct 29 16:59:12 2009 +0100
    29.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Thu Oct 29 17:58:26 2009 +0100
    29.3 @@ -340,7 +340,7 @@
    29.4    case ty  of Eq => k <> 0 | Le => k > 0 | Lt => k >= 0;
    29.5  
    29.6  fun calc_blowup l =
    29.7 -  let val (p,n) = List.partition (curry (op <) 0) (List.filter (curry (op <>) 0) l)
    29.8 +  let val (p,n) = List.partition (curry (op <) 0) (filter (curry (op <>) 0) l)
    29.9    in length p * length n end;
   29.10  
   29.11  (* ------------------------------------------------------------------------- *)
    30.1 --- a/src/Provers/classical.ML	Thu Oct 29 16:59:12 2009 +0100
    30.2 +++ b/src/Provers/classical.ML	Thu Oct 29 17:58:26 2009 +0100
    30.3 @@ -670,7 +670,7 @@
    30.4  (*version of bimatch_from_nets_tac that only applies rules that
    30.5    create precisely n subgoals.*)
    30.6  fun n_bimatch_from_nets_tac n =
    30.7 -    biresolution_from_nets_tac (order_list o List.filter (nsubgoalsP n)) true;
    30.8 +    biresolution_from_nets_tac (order_list o filter (nsubgoalsP n)) true;
    30.9  
   30.10  fun eq_contr_tac i = ematch_tac [not_elim] i  THEN  eq_assume_tac i;
   30.11  val eq_assume_contr_tac = eq_assume_tac ORELSE' eq_contr_tac;
    31.1 --- a/src/Provers/splitter.ML	Thu Oct 29 16:59:12 2009 +0100
    31.2 +++ b/src/Provers/splitter.ML	Thu Oct 29 17:58:26 2009 +0100
    31.3 @@ -192,7 +192,7 @@
    31.4    if n > length ts then []
    31.5    else let val lev = length apsns
    31.6             val lbnos = fold add_lbnos (Library.take (n, ts)) []
    31.7 -           val flbnos = List.filter (fn i => i < lev) lbnos
    31.8 +           val flbnos = filter (fn i => i < lev) lbnos
    31.9             val tt = incr_boundvars (~lev) t
   31.10         in if null flbnos then
   31.11              if T = T' then [(thm,[],pos,TB,tt)] else []
    32.1 --- a/src/Pure/Isar/rule_insts.ML	Thu Oct 29 16:59:12 2009 +0100
    32.2 +++ b/src/Pure/Isar/rule_insts.ML	Thu Oct 29 17:58:26 2009 +0100
    32.3 @@ -268,7 +268,7 @@
    32.4      (* Separate type and term insts *)
    32.5      fun has_type_var ((x, _), _) =
    32.6        (case Symbol.explode x of "'" :: _ => true | _ => false);
    32.7 -    val Tinsts = List.filter has_type_var insts;
    32.8 +    val Tinsts = filter has_type_var insts;
    32.9      val tinsts = filter_out has_type_var insts;
   32.10  
   32.11      (* Tactic *)
    33.1 --- a/src/Pure/Proof/extraction.ML	Thu Oct 29 16:59:12 2009 +0100
    33.2 +++ b/src/Pure/Proof/extraction.ML	Thu Oct 29 17:58:26 2009 +0100
    33.3 @@ -651,7 +651,7 @@
    33.4                      val nt = Envir.beta_norm t;
    33.5                      val args = filter_out (fn v => member (op =) rtypes
    33.6                        (tname_of (body_type (fastype_of v)))) (vfs_of prop);
    33.7 -                    val args' = List.filter (fn v => Logic.occs (v, nt)) args;
    33.8 +                    val args' = filter (fn v => Logic.occs (v, nt)) args;
    33.9                      val t' = mkabs nt args';
   33.10                      val T = fastype_of t';
   33.11                      val cname = extr_name s vs';
    34.1 --- a/src/Pure/Syntax/parser.ML	Thu Oct 29 16:59:12 2009 +0100
    34.2 +++ b/src/Pure/Syntax/parser.ML	Thu Oct 29 17:58:26 2009 +0100
    34.3 @@ -615,11 +615,11 @@
    34.4  
    34.5  
    34.6  (*Get all rhss with precedence >= minPrec*)
    34.7 -fun getRHS minPrec = List.filter (fn (_, _, prec:int) => prec >= minPrec);
    34.8 +fun getRHS minPrec = filter (fn (_, _, prec:int) => prec >= minPrec);
    34.9  
   34.10  (*Get all rhss with precedence >= minPrec and < maxPrec*)
   34.11  fun getRHS' minPrec maxPrec =
   34.12 -  List.filter (fn (_, _, prec:int) => prec >= minPrec andalso prec < maxPrec);
   34.13 +  filter (fn (_, _, prec:int) => prec >= minPrec andalso prec < maxPrec);
   34.14  
   34.15  (*Make states using a list of rhss*)
   34.16  fun mkStates i minPrec lhsID rhss =
   34.17 @@ -655,19 +655,19 @@
   34.18    in update (used, []) end;
   34.19  
   34.20  fun getS A maxPrec Si =
   34.21 -  List.filter
   34.22 +  filter
   34.23      (fn (_, _, _, Nonterminal (B, prec) :: _, _, _)
   34.24            => A = B andalso prec <= maxPrec
   34.25        | _ => false) Si;
   34.26  
   34.27  fun getS' A maxPrec minPrec Si =
   34.28 -  List.filter
   34.29 +  filter
   34.30      (fn (_, _, _, Nonterminal (B, prec) :: _, _, _)
   34.31            => A = B andalso prec > minPrec andalso prec <= maxPrec
   34.32        | _ => false) Si;
   34.33  
   34.34  fun getStates Estate i ii A maxPrec =
   34.35 -  List.filter
   34.36 +  filter
   34.37      (fn (_, _, _, Nonterminal (B, prec) :: _, _, _)
   34.38            => A = B andalso prec <= maxPrec
   34.39        | _ => false)
    35.1 --- a/src/Pure/Syntax/syn_ext.ML	Thu Oct 29 16:59:12 2009 +0100
    35.2 +++ b/src/Pure/Syntax/syn_ext.ML	Thu Oct 29 17:58:26 2009 +0100
    35.3 @@ -218,7 +218,7 @@
    35.4  val read_symbs = map_filter I o the o Scan.read Symbol.stopper scan_symbs;
    35.5  
    35.6  fun unique_index xsymbs =
    35.7 -  if length (List.filter is_index xsymbs) <= 1 then xsymbs
    35.8 +  if length (filter is_index xsymbs) <= 1 then xsymbs
    35.9    else error "Duplicate index arguments (\\<index>)";
   35.10  
   35.11  in
   35.12 @@ -226,7 +226,7 @@
   35.13  val read_mfix = unique_index o read_symbs o Symbol.explode;
   35.14  
   35.15  fun mfix_delims sy = fold_rev (fn Delim s => cons s | _ => I) (read_mfix sy) [];
   35.16 -val mfix_args = length o List.filter is_argument o read_mfix;
   35.17 +val mfix_args = length o filter is_argument o read_mfix;
   35.18  
   35.19  val escape_mfix = implode o map (fn s => if is_meta s then "'" ^ s else s) o Symbol.explode;
   35.20  
   35.21 @@ -276,7 +276,7 @@
   35.22  
   35.23  
   35.24      val raw_symbs = read_mfix sy handle ERROR msg => err_in_mfix msg mfix;
   35.25 -    val args = List.filter (fn Argument _ => true | _ => false) raw_symbs;
   35.26 +    val args = filter (fn Argument _ => true | _ => false) raw_symbs;
   35.27      val (const', typ', parse_rules) =
   35.28        if not (exists is_index args) then (const, typ, [])
   35.29        else
   35.30 @@ -312,7 +312,7 @@
   35.31      val xprod' =
   35.32        if Lexicon.is_terminal lhs' then err_in_mfix ("Illegal lhs: " ^ lhs') mfix
   35.33        else if const <> "" then xprod
   35.34 -      else if length (List.filter is_argument symbs') <> 1 then
   35.35 +      else if length (filter is_argument symbs') <> 1 then
   35.36          err_in_mfix "Copy production must have exactly one argument" mfix
   35.37        else if exists is_terminal symbs' then xprod
   35.38        else XProd (lhs', map rem_pri symbs', "", chain_pri);
    36.1 --- a/src/Pure/codegen.ML	Thu Oct 29 16:59:12 2009 +0100
    36.2 +++ b/src/Pure/codegen.ML	Thu Oct 29 17:58:26 2009 +0100
    36.3 @@ -137,7 +137,7 @@
    36.4    | args_of (Ignore :: ms) (_ :: xs) = args_of ms xs
    36.5    | args_of (_ :: ms) xs = args_of ms xs;
    36.6  
    36.7 -fun num_args_of x = length (List.filter is_arg x);
    36.8 +fun num_args_of x = length (filter is_arg x);
    36.9  
   36.10  
   36.11  (**** theory data ****)
    37.1 --- a/src/Pure/proofterm.ML	Thu Oct 29 16:59:12 2009 +0100
    37.2 +++ b/src/Pure/proofterm.ML	Thu Oct 29 17:58:26 2009 +0100
    37.3 @@ -1024,7 +1024,7 @@
    37.4  
    37.5  (** see pattern.ML **)
    37.6  
    37.7 -fun flt (i: int) = List.filter (fn n => n < i);
    37.8 +fun flt (i: int) = filter (fn n => n < i);
    37.9  
   37.10  fun fomatch Ts tymatch j =
   37.11    let
    38.1 --- a/src/Pure/unify.ML	Thu Oct 29 16:59:12 2009 +0100
    38.2 +++ b/src/Pure/unify.ML	Thu Oct 29 17:58:26 2009 +0100
    38.3 @@ -473,7 +473,7 @@
    38.4        if i<lev then Bound i
    38.5        else  if member (op =) banned (i-lev)
    38.6        then raise CHANGE_FAIL (**flexible occurrence: give up**)
    38.7 -      else  Bound (i - length (List.filter (fn j => j < i-lev) banned))
    38.8 +      else  Bound (i - length (filter (fn j => j < i-lev) banned))
    38.9    | change lev (Abs (a,T,t)) = Abs (a, T, change(lev+1) t)
   38.10    | change lev (t$u) = change lev t $ change lev u
   38.11    | change lev t = t
    39.1 --- a/src/Tools/IsaPlanner/rw_inst.ML	Thu Oct 29 16:59:12 2009 +0100
    39.2 +++ b/src/Tools/IsaPlanner/rw_inst.ML	Thu Oct 29 17:58:26 2009 +0100
    39.3 @@ -169,7 +169,7 @@
    39.4                         OldTerm.add_term_tfrees (t,tfrees)))
    39.5                    ([],[]) ts;
    39.6          val unfixed_tvars = 
    39.7 -            List.filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars;
    39.8 +            filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars;
    39.9          val (fixtyinsts, _) = List.foldr new_tfree ([], map fst tfrees) unfixed_tvars
   39.10      in (fixtyinsts, tfrees) end;
   39.11  
    40.1 --- a/src/ZF/arith_data.ML	Thu Oct 29 16:59:12 2009 +0100
    40.2 +++ b/src/ZF/arith_data.ML	Thu Oct 29 17:58:26 2009 +0100
    40.3 @@ -68,7 +68,7 @@
    40.4  fun prove_conv name tacs ctxt prems (t,u) =
    40.5    if t aconv u then NONE
    40.6    else
    40.7 -  let val prems' = List.filter (not o is_eq_thm) prems
    40.8 +  let val prems' = filter_out is_eq_thm prems
    40.9        val goal = Logic.list_implies (map (#prop o Thm.rep_thm) prems',
   40.10          FOLogic.mk_Trueprop (mk_eq_iff (t, u)));
   40.11    in SOME (prems' MRS Goal.prove ctxt [] [] goal (K (EVERY tacs)))
    41.1 --- a/src/ZF/ind_syntax.ML	Thu Oct 29 16:59:12 2009 +0100
    41.2 +++ b/src/ZF/ind_syntax.ML	Thu Oct 29 17:58:26 2009 +0100
    41.3 @@ -96,8 +96,8 @@
    41.4  fun union_params (rec_tm, cs) =
    41.5    let val (_,args) = strip_comb rec_tm
    41.6        fun is_ind arg = (type_of arg = iT)
    41.7 -  in  case List.filter is_ind (args @ cs) of
    41.8 -         []     => @{const 0}
    41.9 +  in  case filter is_ind (args @ cs) of
   41.10 +         [] => @{const 0}
   41.11         | u_args => Balanced_Tree.make mk_Un u_args
   41.12    end;
   41.13