tuned basic list operators (flat, maps, map_filter);
authorwenzelm
Thu Apr 27 15:06:35 2006 +0200 (2006-04-27)
changeset 194829f11af8f7ef9
parent 19481 a6205c6203ea
child 19483 55ee839198bd
tuned basic list operators (flat, maps, map_filter);
src/Provers/Arith/fast_lin_arith.ML
src/Provers/blast.ML
src/Provers/induct_method.ML
src/Pure/General/graph.ML
src/Pure/General/path.ML
src/Pure/General/pretty.ML
src/Pure/General/table.ML
src/Pure/General/xml.ML
src/Pure/IsaPlanner/isand.ML
src/Pure/IsaPlanner/term_lib.ML
src/Pure/Isar/args.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/context_rules.ML
src/Pure/Isar/element.ML
src/Pure/Isar/find_theorems.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/isar_thy.ML
src/Pure/Isar/local_syntax.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/method.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/outer_parse.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/proof_display.ML
src/Pure/Isar/rule_cases.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_rewrite_rules.ML
src/Pure/Proof/reconstruct.ML
src/Pure/Syntax/lexicon.ML
src/Pure/Syntax/mixfix.ML
src/Pure/Syntax/parser.ML
src/Pure/Syntax/printer.ML
src/Pure/Syntax/syn_ext.ML
src/Pure/Syntax/syn_trans.ML
src/Pure/Syntax/syntax.ML
src/Pure/Thy/thm_database.ML
src/Pure/Thy/thy_info.ML
src/Pure/Tools/am_compiler.ML
src/Pure/Tools/class_package.ML
src/Pure/Tools/codegen_package.ML
src/Pure/Tools/codegen_serializer.ML
src/Pure/Tools/codegen_theorems.ML
src/Pure/Tools/codegen_thingol.ML
src/Pure/Tools/compute.ML
src/Pure/Tools/nbe_codegen.ML
src/Pure/axclass.ML
src/Pure/codegen.ML
src/Pure/consts.ML
src/Pure/context.ML
src/Pure/defs.ML
src/Pure/display.ML
src/Pure/drule.ML
src/Pure/goal.ML
src/Pure/meta_simplifier.ML
src/Pure/net.ML
src/Pure/pattern.ML
src/Pure/proof_general.ML
src/Pure/proofterm.ML
src/Pure/pure_thy.ML
src/Pure/search.ML
src/Pure/sign.ML
src/Pure/sorts.ML
src/Pure/tactic.ML
src/Pure/theory.ML
src/Pure/type_infer.ML
     1.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Thu Apr 27 12:11:56 2006 +0200
     1.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Thu Apr 27 15:06:35 2006 +0200
     1.3 @@ -327,7 +327,7 @@
     1.4  (* ------------------------------------------------------------------------- *)
     1.5  
     1.6  fun allpairs f xs ys =
     1.7 -  List.concat(map (fn x => map (fn y => f x y) ys) xs);
     1.8 +  maps (fn x => map (fn y => f x y) ys) xs;
     1.9  
    1.10  fun extract_first p =
    1.11    let fun extract xs (y::ys) = if p y then (SOME y,xs@ys)
    1.12 @@ -414,7 +414,7 @@
    1.13        val simpset' = Simplifier.inherit_context ss simpset;
    1.14        val atoms = Library.foldl (fn (ats,(lhs,_,_,rhs,_,_)) =>
    1.15                              map fst lhs  union  (map fst rhs  union  ats))
    1.16 -                        ([], List.mapPartial (fn thm => if Thm.no_prems thm
    1.17 +                        ([], map_filter (fn thm => if Thm.no_prems thm
    1.18                                          then LA_Data.decomp sg (concl_of thm)
    1.19                                          else NONE) asms)
    1.20  
    1.21 @@ -596,7 +596,7 @@
    1.22          val mkleq = mklineq n atoms
    1.23          val ixs = 0 upto (n-1)
    1.24          val iatoms = atoms ~~ ixs
    1.25 -        val natlineqs = List.mapPartial (mknat pTs ixs) iatoms
    1.26 +        val natlineqs = map_filter (mknat pTs ixs) iatoms
    1.27          val ineqs = map mkleq initems @ natlineqs
    1.28      in case elim(ineqs,[]) of
    1.29           Success(j) =>
    1.30 @@ -726,7 +726,7 @@
    1.31  *)
    1.32  fun lin_arith_prover sg ss concl =
    1.33  let
    1.34 -    val thms = List.concat(map LA_Logic.atomize (prems_of_ss ss));
    1.35 +    val thms = maps LA_Logic.atomize (prems_of_ss ss);
    1.36      val Hs = map (#prop o rep_thm) thms
    1.37      val Tconcl = LA_Logic.mk_Trueprop concl
    1.38  in case prove sg ([],[]) false Hs Tconcl of (* concl provable? *)
     2.1 --- a/src/Provers/blast.ML	Thu Apr 27 12:11:56 2006 +0200
     2.2 +++ b/src/Provers/blast.ML	Thu Apr 27 15:06:35 2006 +0200
     2.3 @@ -538,16 +538,12 @@
     2.4    case P of
     2.5        (Const ("*Goal*", _) $ G) =>
     2.6          let val pG = mk_Trueprop (toTerm 2 G)
     2.7 -            val intrs = List.concat
     2.8 -                             (map (fn (inet,_) => Net.unify_term inet pG)
     2.9 -                              nps)
    2.10 +            val intrs = maps (fn (inet,_) => Net.unify_term inet pG) nps
    2.11          in  map (fromIntrRule vars o #2) (Tactic.orderlist intrs)  end
    2.12      | _ =>
    2.13          let val pP = mk_Trueprop (toTerm 3 P)
    2.14 -            val elims = List.concat
    2.15 -                             (map (fn (_,enet) => Net.unify_term enet pP)
    2.16 -                              nps)
    2.17 -        in  List.mapPartial (fromRule vars o #2) (Tactic.orderlist elims)  end;
    2.18 +            val elims = maps (fn (_,enet) => Net.unify_term enet pP) nps
    2.19 +        in  map_filter (fromRule vars o #2) (Tactic.orderlist elims)  end;
    2.20  
    2.21  
    2.22  (*Pending formulae carry md (may duplicate) flags*)
     3.1 --- a/src/Provers/induct_method.ML	Thu Apr 27 12:11:56 2006 +0200
     3.2 +++ b/src/Provers/induct_method.ML	Thu Apr 27 15:06:35 2006 +0200
     3.3 @@ -80,7 +80,7 @@
     3.4      val xs = InductAttrib.vars_of tm;
     3.5    in
     3.6      align "Rule has fewer variables than instantiations given" xs ts
     3.7 -    |> List.mapPartial prep_var
     3.8 +    |> map_filter prep_var
     3.9    end;
    3.10  
    3.11  
    3.12 @@ -129,7 +129,7 @@
    3.13      fun inst_rule r =
    3.14        if null insts then `RuleCases.get r
    3.15        else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
    3.16 -        |> (List.concat o map (prep_inst thy align_left I))
    3.17 +        |> maps (prep_inst thy align_left I)
    3.18          |> Drule.cterm_instantiate) r |> pair (RuleCases.get r);
    3.19  
    3.20      val ruleq =
    3.21 @@ -333,7 +333,7 @@
    3.22            in ((SOME (Free lhs), [def]), ctxt') end
    3.23        | add (SOME (NONE, t)) ctxt = ((SOME t, []), ctxt)
    3.24        | add NONE ctxt = ((NONE, []), ctxt);
    3.25 -  in fold_map add def_insts #> apfst (split_list #> apsnd List.concat) end;
    3.26 +  in fold_map add def_insts #> apfst (split_list #> apsnd flat) end;
    3.27  
    3.28  
    3.29  (* induct_tac *)
    3.30 @@ -348,7 +348,7 @@
    3.31  local
    3.32  
    3.33  fun find_inductT ctxt insts =
    3.34 -  fold_rev multiply (insts |> List.mapPartial (fn [] => NONE | ts => List.last ts)
    3.35 +  fold_rev multiply (insts |> map_filter (fn [] => NONE | ts => List.last ts)
    3.36      |> map (InductAttrib.find_inductT ctxt o Term.fastype_of)) [[]]
    3.37    |> filter_out (forall PureThy.is_internal);
    3.38  
    3.39 @@ -370,7 +370,7 @@
    3.40        (if null insts then `RuleCases.get r
    3.41         else (align_left "Rule has fewer conclusions than arguments given"
    3.42            (map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
    3.43 -        |> (List.concat o map (prep_inst thy align_right (atomize_term thy)))
    3.44 +        |> maps (prep_inst thy align_right (atomize_term thy))
    3.45          |> Drule.cterm_instantiate) r |> pair (RuleCases.get r))
    3.46        |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
    3.47  
    3.48 @@ -380,7 +380,7 @@
    3.49        | NONE =>
    3.50            (find_inductS ctxt facts @
    3.51              map (special_rename_params defs_ctxt insts) (find_inductT ctxt insts))
    3.52 -          |> List.mapPartial RuleCases.mutual_rule
    3.53 +          |> map_filter RuleCases.mutual_rule
    3.54            |> tap (trace_rules ctxt InductAttrib.inductN o map #2)
    3.55            |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
    3.56  
    3.57 @@ -389,7 +389,7 @@
    3.58    in
    3.59      (fn i => fn st =>
    3.60        ruleq
    3.61 -      |> Seq.maps (RuleCases.consume (List.concat defs) facts)
    3.62 +      |> Seq.maps (RuleCases.consume (flat defs) facts)
    3.63        |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
    3.64          (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
    3.65            (CONJUNCTS (ALLGOALS
     4.1 --- a/src/Pure/General/graph.ML	Thu Apr 27 12:11:56 2006 +0200
     4.2 +++ b/src/Pure/General/graph.ML	Thu Apr 27 15:06:35 2006 +0200
     4.3 @@ -132,13 +132,13 @@
     4.4  fun imm_succs G = #2 o #2 o get_entry G;
     4.5  
     4.6  (*transitive*)
     4.7 -fun all_preds G = List.concat o fst o reachable (imm_preds G);
     4.8 -fun all_succs G = List.concat o fst o reachable (imm_succs G);
     4.9 +fun all_preds G = flat o fst o reachable (imm_preds G);
    4.10 +fun all_succs G = flat o fst o reachable (imm_succs G);
    4.11  
    4.12  (*strongly connected components; see: David King and John Launchbury,
    4.13    "Structuring Depth First Search Algorithms in Haskell"*)
    4.14  fun strong_conn G = filter_out null (fst (reachable (imm_preds G)
    4.15 -  (List.concat (rev (fst (reachable (imm_succs G) (keys G)))))));
    4.16 +  (flat (rev (fst (reachable (imm_succs G) (keys G)))))));
    4.17  
    4.18  (*subgraph induced by node subset*)
    4.19  fun subgraph keys (Graph tab) =
    4.20 @@ -157,7 +157,7 @@
    4.21      fun paths ps p =
    4.22        if not (null ps) andalso eq_key (p, x) then [p :: ps]
    4.23        else if member_keys X p andalso not (member_key ps p)
    4.24 -      then List.concat (map (paths (p :: ps)) (imm_preds G p))
    4.25 +      then maps (paths (p :: ps)) (imm_preds G p)
    4.26        else [];
    4.27    in paths [] y end;
    4.28  
    4.29 @@ -194,7 +194,7 @@
    4.30    else G;
    4.31  
    4.32  fun diff_edges G1 G2 =
    4.33 -  List.concat (dest G1 |> map (fn (x, ys) => ys |> List.mapPartial (fn y =>
    4.34 +  flat (dest G1 |> map (fn (x, ys) => ys |> map_filter (fn y =>
    4.35      if is_edge G2 (x, y) then NONE else SOME (x, y))));
    4.36  
    4.37  fun edges G = diff_edges G empty;
     5.1 --- a/src/Pure/General/path.ML	Thu Apr 27 12:11:56 2006 +0200
     5.2 +++ b/src/Pure/General/path.ML	Thu Apr 27 15:06:35 2006 +0200
     5.3 @@ -153,7 +153,7 @@
     5.4      | path => rep (unpack path))
     5.5    | eval x = [x];
     5.6  
     5.7 -val expand = rep #> map eval #> List.concat #> norm #> Path;
     5.8 +val expand = rep #> maps eval #> norm #> Path;
     5.9  val position = expand #> pack #> quote #> Position.line_name 1;
    5.10  
    5.11  end;
     6.1 --- a/src/Pure/General/pretty.ML	Thu Apr 27 12:11:56 2006 +0200
     6.2 +++ b/src/Pure/General/pretty.ML	Thu Apr 27 15:06:35 2006 +0200
     6.3 @@ -219,13 +219,13 @@
     6.4  
     6.5  val strs = block o breaks o map str;
     6.6  fun chunks prts = blk (0, fbreaks prts);
     6.7 -fun chunks2 prts = blk (0, List.concat (Library.separate [fbrk, fbrk] (map single prts)));
     6.8 +fun chunks2 prts = blk (0, flat (Library.separate [fbrk, fbrk] (map single prts)));
     6.9  
    6.10  fun quote prt = blk (1, [str "\"", prt, str "\""]);
    6.11  fun backquote prt = blk (1, [str "`", prt, str "`"]);
    6.12  
    6.13  fun separate sep prts =
    6.14 -  List.concat (Library.separate [str sep, brk 1] (map single prts));
    6.15 +  flat (Library.separate [str sep, brk 1] (map single prts));
    6.16  
    6.17  val commas = separate ",";
    6.18  
     7.1 --- a/src/Pure/General/table.ML	Thu Apr 27 12:11:56 2006 +0200
     7.2 +++ b/src/Pure/General/table.ML	Thu Apr 27 15:06:35 2006 +0200
     7.3 @@ -379,7 +379,7 @@
     7.4    handle UNDEF _ => delete key tab;
     7.5  
     7.6  fun make_list args = fold_rev update_list args empty;
     7.7 -fun dest_list tab = List.concat (map (fn (key, xs) => map (pair key) xs) (dest tab));
     7.8 +fun dest_list tab = maps (fn (key, xs) => map (pair key) xs) (dest tab);
     7.9  fun merge_list eq = join (fn _ => Library.merge eq);
    7.10  
    7.11  
     8.1 --- a/src/Pure/General/xml.ML	Thu Apr 27 12:11:56 2006 +0200
     8.2 +++ b/src/Pure/General/xml.ML	Thu Apr 27 15:06:35 2006 +0200
     8.3 @@ -134,7 +134,7 @@
     8.4          || parse_pi >> K []
     8.5          || parse_comment >> K []) --
     8.6         Scan.optional ((* scan_whspc |-- *) parse_chars >> (single o Text)) []
     8.7 -         >> op @) >> List.concat) >> op @)(* --| scan_whspc*)) xs
     8.8 +         >> op @) >> flat) >> op @)(* --| scan_whspc*)) xs
     8.9  
    8.10  and parse_elem xs =
    8.11    ($$ "<" |-- Symbol.scan_id --
     9.1 --- a/src/Pure/IsaPlanner/isand.ML	Thu Apr 27 12:11:56 2006 +0200
     9.2 +++ b/src/Pure/IsaPlanner/isand.ML	Thu Apr 27 15:06:35 2006 +0200
     9.3 @@ -257,7 +257,7 @@
     9.4        val prop = (Thm.prop_of th);
     9.5        val tvars = List.foldr Term.add_term_tvars [] (prop :: tpairs);
     9.6        val ctyfixes = 
     9.7 -          Library.mapfilter 
     9.8 +          map_filter 
     9.9              (fn (v as ((s,i),ty)) => 
    9.10                  if i <= ix then SOME (ctypify (TVar v), ctypify (TFree (s,ty)))
    9.11                  else NONE) tvars;
    9.12 @@ -271,7 +271,7 @@
    9.13        val vars = map Term.dest_Var (List.foldr Term.add_term_vars 
    9.14                                                 [] (prop :: tpairs));
    9.15        val cfixes = 
    9.16 -          Library.mapfilter 
    9.17 +          map_filter 
    9.18              (fn (v as ((s,i),ty)) => 
    9.19                  if i <= ix then SOME (ctermify (Var v), ctermify (Free (s,ty)))
    9.20                  else NONE) vars;
    10.1 --- a/src/Pure/IsaPlanner/term_lib.ML	Thu Apr 27 12:11:56 2006 +0200
    10.2 +++ b/src/Pure/IsaPlanner/term_lib.ML	Thu Apr 27 15:06:35 2006 +0200
    10.3 @@ -428,8 +428,7 @@
    10.4    | term_contains1 T (ah $ at) (bh $ bt) =
    10.5      (term_contains1 T ah (bh $ bt)) @
    10.6      (term_contains1 T at (bh $ bt)) @
    10.7 -    (List.concat (map (fn inT => (term_contains1 inT at bt))
    10.8 -               (term_contains1 T ah bh)))
    10.9 +    (maps (fn inT => (term_contains1 inT at bt)) (term_contains1 T ah bh))
   10.10  
   10.11    | term_contains1 T a (bh $ bt) = []
   10.12  
    11.1 --- a/src/Pure/Isar/args.ML	Thu Apr 27 12:11:56 2006 +0200
    11.2 +++ b/src/Pure/Isar/args.ML	Thu Apr 27 15:06:35 2006 +0200
    11.3 @@ -352,7 +352,7 @@
    11.4    ((Scan.repeat1
    11.5      (Scan.repeat1 (atomic blk) ||
    11.6        argsp "(" ")" ||
    11.7 -      argsp "[" "]")) >> List.concat) x
    11.8 +      argsp "[" "]")) >> flat) x
    11.9  and argsp l r x =
   11.10    (Scan.trace (&&& l -- !!! (args true -- &&& r)) >> #2) x;
   11.11  
    12.1 --- a/src/Pure/Isar/attrib.ML	Thu Apr 27 12:11:56 2006 +0200
    12.2 +++ b/src/Pure/Isar/attrib.ML	Thu Apr 27 15:06:35 2006 +0200
    12.3 @@ -164,7 +164,7 @@
    12.4  
    12.5  val thm = gen_thm PureThy.single_thm;
    12.6  val multi_thm = gen_thm (K I);
    12.7 -val thms = Scan.repeat multi_thm >> List.concat;
    12.8 +val thms = Scan.repeat multi_thm >> flat;
    12.9  
   12.10  end;
   12.11  
   12.12 @@ -250,11 +250,11 @@
   12.13      val ctxt = Context.proof_of generic;
   12.14  
   12.15      val (type_insts, term_insts) = List.partition (is_tvar o fst) (map snd mixed_insts);
   12.16 -    val internal_insts = term_insts |> List.mapPartial
   12.17 +    val internal_insts = term_insts |> map_filter
   12.18        (fn (xi, Args.Term t) => SOME (xi, t)
   12.19        | (_, Args.Name _) => NONE
   12.20        | (xi, _) => error_var "Term argument expected for " xi);
   12.21 -    val external_insts = term_insts |> List.mapPartial
   12.22 +    val external_insts = term_insts |> map_filter
   12.23        (fn (xi, Args.Name s) => SOME (xi, s) | _ => NONE);
   12.24  
   12.25  
    13.1 --- a/src/Pure/Isar/context_rules.ML	Thu Apr 27 12:11:56 2006 +0200
    13.2 +++ b/src/Pure/Isar/context_rules.ML	Thu Apr 27 15:06:35 2006 +0200
    13.3 @@ -118,7 +118,7 @@
    13.4        val ctxt = Context.proof_of generic;
    13.5        fun prt_kind (i, b) =
    13.6          Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":")
    13.7 -          (List.mapPartial (fn (_, (k, th)) =>
    13.8 +          (map_filter (fn (_, (k, th)) =>
    13.9                if k = (i, b) then SOME (ProofContext.pretty_thm ctxt th) else NONE)
   13.10              (sort (int_ord o pairself fst) rules));
   13.11      in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
    14.1 --- a/src/Pure/Isar/element.ML	Thu Apr 27 12:11:56 2006 +0200
    14.2 +++ b/src/Pure/Isar/element.ML	Thu Apr 27 15:06:35 2006 +0200
    14.3 @@ -100,7 +100,7 @@
    14.4        |> Option.map (fn v => (certT (TVar v), certT T));
    14.5    in
    14.6      Drule.tvars_intr_list (map fst subst) #->
    14.7 -    (fn vs => Thm.instantiate (List.mapPartial (inst vs) subst, []))
    14.8 +    (fn vs => Thm.instantiate (map_filter (inst vs) subst, []))
    14.9    end;
   14.10  
   14.11  fun instantiate_frees thy subst =
   14.12 @@ -144,7 +144,7 @@
   14.13  fun rename_thm ren th =
   14.14    let
   14.15      val subst = Drule.frees_of th
   14.16 -      |> List.mapPartial (fn (x, T) =>
   14.17 +      |> map_filter (fn (x, T) =>
   14.18          let val x' = rename ren x
   14.19          in if x = x' then NONE else SOME ((x, T), (Free (x', T))) end);
   14.20    in
   14.21 @@ -169,7 +169,7 @@
   14.22  
   14.23  fun instT_subst env th =
   14.24    Drule.tfrees_of th
   14.25 -  |> List.mapPartial (fn (a, S) =>
   14.26 +  |> map_filter (fn (a, S) =>
   14.27      let
   14.28        val T = TFree (a, S);
   14.29        val T' = the_default T (Symtab.lookup env a);
   14.30 @@ -209,7 +209,7 @@
   14.31      let
   14.32        val substT = instT_subst envT th;
   14.33        val subst = Drule.frees_of th
   14.34 -        |> List.mapPartial (fn (x, T) =>
   14.35 +        |> map_filter (fn (x, T) =>
   14.36            let
   14.37              val T' = instT_type envT T;
   14.38              val t = Free (x, T');
   14.39 @@ -291,7 +291,7 @@
   14.40        | prt_fact (ths, atts) = Pretty.enclose "(" ")"
   14.41            (Pretty.breaks (map prt_thm ths)) :: Args.pretty_attribs ctxt atts;
   14.42      fun prt_note (a, ths) =
   14.43 -      Pretty.block (Pretty.breaks (List.concat (prt_name_atts a "=" :: map prt_fact ths)));
   14.44 +      Pretty.block (Pretty.breaks (flat (prt_name_atts a "=" :: map prt_fact ths)));
   14.45    in
   14.46      fn Fixes fixes => pretty_items "fixes" "and" (map prt_fix fixes)
   14.47       | Constrains xs => pretty_items "constrains" "and" (map prt_constrain xs)
    15.1 --- a/src/Pure/Isar/find_theorems.ML	Thu Apr 27 12:11:56 2006 +0200
    15.2 +++ b/src/Pure/Isar/find_theorems.ML	Thu Apr 27 15:06:35 2006 +0200
    15.3 @@ -93,7 +93,7 @@
    15.4      val match_thm = matches o refine_term;
    15.5    in
    15.6      map (substsize o refine_term)
    15.7 -        (List.filter match_thm (extract_terms term_src)) |> bestmatch
    15.8 +        (filter match_thm (extract_terms term_src)) |> bestmatch
    15.9    end;
   15.10  
   15.11  
   15.12 @@ -124,7 +124,7 @@
   15.13      val prems = Logic.prems_of_goal goal 1;
   15.14  
   15.15      fun try_subst prem = is_matching_thm extract_dest ctxt true prem thm;
   15.16 -    val successful = prems |> List.mapPartial try_subst;
   15.17 +    val successful = prems |> map_filter try_subst;
   15.18    in
   15.19      (*if possible, keep best substitution (one with smallest size)*)
   15.20      (*dest rules always have assumptions, so a dest with one
   15.21 @@ -155,7 +155,7 @@
   15.22        fun goal_tree prem = (combine prem goal_concl);
   15.23        fun try_subst prem =
   15.24          is_matching_thm (single, I) ctxt true (goal_tree prem) rule_tree;
   15.25 -      val successful = prems |> List.mapPartial try_subst;
   15.26 +      val successful = prems |> map_filter try_subst;
   15.27      in
   15.28      (*elim rules always have assumptions, so an elim with one
   15.29        assumption is as good as an intro rule with none*)
   15.30 @@ -226,7 +226,7 @@
   15.31        prod_ord int_ord int_ord ((p1, s1), (p0, s0));
   15.32    in
   15.33      map (`(eval_filters filters)) thms
   15.34 -    |> List.mapPartial (fn (SOME x, y) => SOME (x, y) | (NONE, _) => NONE)
   15.35 +    |> map_filter (fn (SOME x, y) => SOME (x, y) | (NONE, _) => NONE)
   15.36      |> sort thm_ord |> map #2
   15.37    end;
   15.38  
   15.39 @@ -237,11 +237,9 @@
   15.40  
   15.41  fun find_thms ctxt spec =
   15.42    (PureThy.thms_containing (ProofContext.theory_of ctxt) spec
   15.43 -    |> map PureThy.selections
   15.44 -    |> List.concat) @
   15.45 +    |> maps PureThy.selections) @
   15.46    (ProofContext.lthms_containing ctxt spec
   15.47 -    |> map PureThy.selections
   15.48 -    |> List.concat
   15.49 +    |> maps PureThy.selections
   15.50      |> distinct (fn ((r1, th1), (r2, th2)) =>
   15.51          r1 = r2 andalso Drule.eq_thm_prop (th1, th2)));
   15.52  
    16.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Apr 27 12:11:56 2006 +0200
    16.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Apr 27 15:06:35 2006 +0200
    16.3 @@ -239,7 +239,7 @@
    16.4  
    16.5  val declareP =
    16.6    OuterSyntax.command "declare" "declare theorems (improper)" K.thy_script
    16.7 -    (P.opt_locale_target -- (P.and_list1 P.xthms1 >> List.concat)
    16.8 +    (P.opt_locale_target -- (P.and_list1 P.xthms1 >> flat)
    16.9        >> (Toplevel.theory_context o uncurry IsarThy.declare_theorems));
   16.10  
   16.11  
    17.1 --- a/src/Pure/Isar/isar_thy.ML	Thu Apr 27 12:11:56 2006 +0200
    17.2 +++ b/src/Pure/Isar/isar_thy.ML	Thu Apr 27 15:06:35 2006 +0200
    17.3 @@ -80,8 +80,8 @@
    17.4    PureThy.note_thmss_i kind args
    17.5    #> tap (present_theorems kind);
    17.6  
    17.7 -fun apply_theorems args = apfst (List.concat o map snd) o theorems "" [(("", []), args)];
    17.8 -fun apply_theorems_i args = apfst (List.concat o map snd) o theorems_i "" [(("", []), args)];
    17.9 +fun apply_theorems args = apfst (maps snd) o theorems "" [(("", []), args)];
   17.10 +fun apply_theorems_i args = apfst (maps snd) o theorems_i "" [(("", []), args)];
   17.11  
   17.12  fun smart_theorems kind NONE args thy = thy
   17.13        |> theorems kind args
    18.1 --- a/src/Pure/Isar/local_syntax.ML	Thu Apr 27 12:11:56 2006 +0200
    18.2 +++ b/src/Pure/Isar/local_syntax.ML	Thu Apr 27 15:06:35 2006 +0200
    18.3 @@ -104,7 +104,7 @@
    18.4        let
    18.5          val mixfixes' = mixfixes |> fold (add_mixfix prmode) (filter_out mixfix_struct decls);
    18.6          val fixes' = fold (fn (((x, true), _), _) => cons x | _ => I) mixfixes' [];
    18.7 -        val structs' = structs @ List.mapPartial prep_struct decls;
    18.8 +        val structs' = structs @ map_filter prep_struct decls;
    18.9        in build_syntax thy (mixfixes', (structs', fixes')) end);
   18.10  
   18.11  end;
    19.1 --- a/src/Pure/Isar/locale.ML	Thu Apr 27 12:11:56 2006 +0200
    19.2 +++ b/src/Pure/Isar/locale.ML	Thu Apr 27 15:06:35 2006 +0200
    19.3 @@ -201,7 +201,7 @@
    19.4  
    19.5    (* registrations that subsume t *)
    19.6    fun subsumers thy t regs =
    19.7 -    List.filter (fn (t', _) => Pattern.matches thy (t', t)) (Termtab.dest regs);
    19.8 +    filter (fn (t', _) => Pattern.matches thy (t', t)) (Termtab.dest regs);
    19.9  
   19.10    (* look up registration, pick one that subsumes the query *)
   19.11    fun lookup sign (regs, ts) =
   19.12 @@ -235,7 +235,7 @@
   19.13      in (case subs of
   19.14          [] => let
   19.15                  val sups =
   19.16 -                  List.filter (fn (t', _) => Pattern.matches sign (t, t')) (Termtab.dest regs);
   19.17 +                  filter (fn (t', _) => Pattern.matches sign (t, t')) (Termtab.dest regs);
   19.18                  val sups' = map (apfst untermify) sups
   19.19                in (Termtab.update (t, (attn, [])) regs, sups') end
   19.20        | _ => (regs, []))
   19.21 @@ -480,7 +480,7 @@
   19.22      val thy = ProofContext.theory_of ctxt;
   19.23      fun prt_id (name, parms) =
   19.24        [Pretty.block (Pretty.breaks (map Pretty.str (extern thy name :: parms)))];
   19.25 -    val prt_ids = List.concat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids));
   19.26 +    val prt_ids = flat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids));
   19.27      val err_msg =
   19.28        if forall (equal "" o #1) ids then msg
   19.29        else msg ^ "\n" ^ Pretty.string_of (Pretty.block
   19.30 @@ -537,19 +537,19 @@
   19.31        | unify _ env = env;
   19.32      val (unifier, _) = fold unify (Ts' ~~ Us') (Vartab.empty, maxidx'');
   19.33      val Vs = map (Option.map (Envir.norm_type unifier)) Us';
   19.34 -    val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (List.mapPartial I Vs));
   19.35 +    val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map_filter I Vs));
   19.36    in map (Option.map (Envir.norm_type unifier')) Vs end;
   19.37  
   19.38 -fun params_of elemss = distinct (eq_fst (op =)) (List.concat (map (snd o fst) elemss));
   19.39 -fun params_of' elemss = distinct (eq_fst (op =)) (List.concat (map (snd o fst o fst) elemss));
   19.40 +fun params_of elemss = distinct (eq_fst (op =)) (maps (snd o fst) elemss);
   19.41 +fun params_of' elemss = distinct (eq_fst (op =)) (maps (snd o fst o fst) elemss);
   19.42  fun params_syn_of syn elemss =
   19.43 -  distinct (eq_fst (op =)) (List.concat (map (snd o fst) elemss)) |>
   19.44 +  distinct (eq_fst (op =)) (maps (snd o fst) elemss) |>
   19.45      map (apfst (fn x => (x, the (Symtab.lookup syn x))));
   19.46  
   19.47  
   19.48  (* CB: param_types has the following type:
   19.49    ('a * 'b option) list -> ('a * 'b) list *)
   19.50 -fun param_types ps = List.mapPartial (fn (_, NONE) => NONE | (x, SOME T) => SOME (x, T)) ps;
   19.51 +fun param_types ps = map_filter (fn (_, NONE) => NONE | (x, SOME T) => SOME (x, T)) ps;
   19.52  
   19.53  
   19.54  fun merge_syntax ctxt ids ss = Symtab.merge (op =) ss
   19.55 @@ -577,7 +577,7 @@
   19.56  fun unique_parms ctxt elemss =
   19.57    let
   19.58      val param_decls =
   19.59 -      List.concat (map (fn (((name, (ps, qs)), _), _) => map (rpair (name, ps)) qs) elemss)
   19.60 +      maps (fn (((name, (ps, qs)), _), _) => map (rpair (name, ps)) qs) elemss
   19.61        |> Symtab.make_list |> Symtab.dest;
   19.62    in
   19.63      (case find_first (fn (_, ids) => length ids > 1) param_decls of
   19.64 @@ -594,7 +594,7 @@
   19.65  
   19.66      fun varify i = Term.map_type_tfree (fn (a, S) => TVar ((a, i), S));
   19.67      fun varify_parms (i, ps) = map (apsnd (varify i)) (param_types ps);
   19.68 -    val parms = fixed_parms @ List.concat (map varify_parms idx_parmss);
   19.69 +    val parms = fixed_parms @ maps varify_parms idx_parmss;
   19.70  
   19.71      fun unify T U envir = Sign.typ_unify thy (U, T) envir
   19.72        handle Type.TUNIFY =>
   19.73 @@ -611,8 +611,8 @@
   19.74      val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms'));
   19.75  
   19.76      fun inst_parms (i, ps) =
   19.77 -      foldr Term.add_typ_tfrees [] (List.mapPartial snd ps)
   19.78 -      |> List.mapPartial (fn (a, S) =>
   19.79 +      foldr Term.add_typ_tfrees [] (map_filter snd ps)
   19.80 +      |> map_filter (fn (a, S) =>
   19.81            let val T = Envir.norm_type unifier' (TVar ((a, i), S))
   19.82            in if T = TFree (a, S) then NONE else SOME (a, T) end)
   19.83        |> Symtab.make;
   19.84 @@ -716,7 +716,7 @@
   19.85            val new_ids' = map (fn (id, ths) =>
   19.86                (id, ([], Derived ths))) (new_ids ~~ new_ths);
   19.87          in
   19.88 -          fold add_regs new_idTs (ths @ List.concat new_ths, ids @ new_ids')
   19.89 +          fold add_regs new_idTs (ths @ flat new_ths, ids @ new_ids')
   19.90          end;
   19.91  
   19.92      (* distribute top-level axioms over assumed ids *)
   19.93 @@ -724,10 +724,10 @@
   19.94      fun axiomify all_ps ((name, parms), (_, Assumed _)) axioms =
   19.95          let
   19.96            val {elems, ...} = the_locale thy name;
   19.97 -          val ts = List.concat (map
   19.98 -            (fn (Assumes asms, _) => List.concat (map (map #1 o #2) asms)
   19.99 +          val ts = maps
  19.100 +            (fn (Assumes asms, _) => maps (map #1 o #2) asms
  19.101                | _ => [])
  19.102 -            elems);
  19.103 +            elems;
  19.104            val (axs1, axs2) = chop (length ts) axioms;
  19.105          in (((name, parms), (all_ps, Assumed axs1)), axs2) end
  19.106        | axiomify all_ps (id, (_, Derived ths)) axioms =
  19.107 @@ -762,7 +762,7 @@
  19.108                handle ERROR msg => err_in_locale' ctxt msg ids';
  19.109  
  19.110              val ids'' = distinct (eq_fst (op =)) (map (rename_parms top ren) ids');
  19.111 -            val parms'' = distinct (op =) (List.concat (map (#2 o #1) ids''));
  19.112 +            val parms'' = distinct (op =) (maps (#2 o #1) ids'');
  19.113              val syn'' = syn' |> Symtab.dest |> map (Element.rename_var ren) |> Symtab.make;
  19.114              (* check for conflicting syntax? *)
  19.115            in (ids'', parms'', syn'') end
  19.116 @@ -849,7 +849,7 @@
  19.117    | activate_elem _ ((ctxt, Assumed axs), Assumes asms) =
  19.118        let
  19.119          val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms;
  19.120 -        val ts = List.concat (map (map #1 o #2) asms');
  19.121 +        val ts = maps (map #1 o #2) asms';
  19.122          val (ps, qs) = chop (length ts) axs;
  19.123          val (_, ctxt') =
  19.124            ctxt |> fold ProofContext.fix_frees ts
  19.125 @@ -895,7 +895,7 @@
  19.126      fold_map (fn (((name, ps), mode), raw_elems) => fn ctxt =>
  19.127        let
  19.128          val elems = map (prep_facts ctxt) raw_elems;
  19.129 -        val (ctxt', res) = apsnd List.concat
  19.130 +        val (ctxt', res) = apsnd flat
  19.131              (activate_elems (((name, ps), mode), elems) ctxt);
  19.132          val elems' = elems |> map (Element.map_ctxt
  19.133            {name = I, var = I, typ = I, term = I, fact = I, attrib = Args.closure});
  19.134 @@ -916,7 +916,7 @@
  19.135  
  19.136  fun activate_facts prep_facts (ctxt, args) =
  19.137    let val ((elemss, factss), ctxt') = activate_elemss prep_facts args ctxt |>> split_list
  19.138 -  in (ctxt', (elemss, List.concat factss)) end;
  19.139 +  in (ctxt', (elemss, flat factss)) end;
  19.140  
  19.141  end;
  19.142  
  19.143 @@ -1047,7 +1047,7 @@
  19.144        fold ProofContext.declare_term (map Free fixed_params) ctxt;
  19.145      val int_elemss =
  19.146        raw_elemss
  19.147 -      |> List.mapPartial (fn (id, Int es) => SOME (id, es) | _ => NONE)
  19.148 +      |> map_filter (fn (id, Int es) => SOME (id, es) | _ => NONE)
  19.149        |> unify_elemss ctxt_with_fixed fixed_params;
  19.150      val (_, raw_elemss') =
  19.151        foldl_map (fn ((_, es) :: elemss, (id, Int _)) => (elemss, (id, Int es)) | x => x)
  19.152 @@ -1086,7 +1086,7 @@
  19.153    | eval_text _ (_, Assumed _) is_ext (Assumes asms)
  19.154          (((exts, exts'), (ints, ints')), (xs, env, defs)) =
  19.155        let
  19.156 -        val ts = List.concat (map (map #1 o #2) asms);
  19.157 +        val ts = maps (map #1 o #2) asms;
  19.158          val ts' = map (norm_term env) ts;
  19.159          val spec' =
  19.160            if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints'))
  19.161 @@ -1165,7 +1165,7 @@
  19.162          val [(id' as (_, mode), es)] = unify_elemss ctxt parms [(id, e)];
  19.163          val wits' = case mode of Assumed _ => wits | Derived ths => wits @ ths;
  19.164          val text' = fold (eval_text ctxt id' false) es text;
  19.165 -        val es' = List.mapPartial
  19.166 +        val es' = map_filter
  19.167                (finish_derived (ProofContext.theory_of ctxt) wits' mode) es;
  19.168        in ((text', wits'), (id', map Int es')) end
  19.169    | finish_elems ctxt parms do_close ((text, wits), ((id, Ext e), [propp])) =
  19.170 @@ -1214,7 +1214,7 @@
  19.171          val (ctxt, all_propp) =
  19.172            prepp (fold ProofContext.declare_term (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp);
  19.173          (* CB: add type information from conclusion and external elements to context *)
  19.174 -        val ctxt = fold ProofContext.declare_term (List.concat (map (map fst) all_propp)) ctxt;
  19.175 +        val ctxt = fold ProofContext.declare_term (maps (map fst) all_propp) ctxt;
  19.176          (* CB: resolve schematic variables (patterns) in conclusion and external elements. *)
  19.177          val all_propp' = map2 (curry (op ~~))
  19.178            (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp)))) (map (map snd) all_propp);
  19.179 @@ -1307,9 +1307,9 @@
  19.180    in
  19.181      elemss |> get
  19.182        |> map (fn (_, es) => map (fn Int e => e) es)
  19.183 -      |> Library.flat
  19.184 -      |> Library.mapfilter (fn Assumes asms => SOME asms | _ => NONE)
  19.185 -      |> Library.flat
  19.186 +      |> flat
  19.187 +      |> map_filter (fn Assumes asms => SOME asms | _ => NONE)
  19.188 +      |> flat
  19.189        |> map (apsnd (map fst))
  19.190    end;
  19.191  
  19.192 @@ -1350,7 +1350,7 @@
  19.193      val ((ids, syn), raw_elemsss) = foldl_map (flatten (context, prep_expr thy))
  19.194        ((import_ids, import_syn), elements);
  19.195  
  19.196 -    val raw_elemss = List.concat raw_elemsss;
  19.197 +    val raw_elemss = flat raw_elemsss;
  19.198      (* CB: raw_import_elemss @ raw_elemss is the normalised list of
  19.199         context elements obtained from import and elements. *)
  19.200      val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close
  19.201 @@ -1368,9 +1368,8 @@
  19.202      val (ctxt, (elemss, _)) =
  19.203        activate_facts prep_facts (import_ctxt, qs);
  19.204      val stmt = distinct Term.aconv
  19.205 -       (List.concat (map (fn ((_, Assumed axs), _) =>
  19.206 -         List.concat (map (#hyps o Thm.rep_thm o #2) axs)
  19.207 -                           | ((_, Derived _), _) => []) qs));
  19.208 +       (maps (fn ((_, Assumed axs), _) => maps (#hyps o Thm.rep_thm o #2) axs
  19.209 +                           | ((_, Derived _), _) => []) qs);
  19.210      val cstmt = map (cterm_of thy) stmt;
  19.211    in
  19.212      ((((import_ctxt, import_elemss), (ctxt, elemss, syn)), (parms, spec, defs)), (cstmt, concl))
  19.213 @@ -1411,7 +1410,7 @@
  19.214      val (((_, import_elemss), (ctxt, elemss, _)), _) =
  19.215        read_context import body (ProofContext.init thy);
  19.216      val prt_elem = Element.pretty_ctxt ctxt;
  19.217 -    val all_elems = List.concat (map #2 (import_elemss @ elemss));
  19.218 +    val all_elems = maps #2 (import_elemss @ elemss);
  19.219    in
  19.220      Pretty.big_list "locale elements:" (all_elems
  19.221        |> (if show_facts then I else filter (fn Notes _ => false | _ => true))
  19.222 @@ -1456,7 +1455,7 @@
  19.223      fun vinst_names ps = map (the o Symtab.lookup vinst) ps;
  19.224      val inst = Symtab.make (parms ~~ ts);
  19.225      val ids' = map (apsnd vinst_names) ids;
  19.226 -    val wits = List.concat (map (snd o the o get_global_registration thy) ids');
  19.227 +    val wits = maps (snd o the o get_global_registration thy) ids';
  19.228    in ((tinst, inst), wits) end;
  19.229  
  19.230  
  19.231 @@ -1468,7 +1467,7 @@
  19.232      val parms = the_locale thy target |> #params |> map fst;
  19.233      val ids = flatten (ProofContext.init thy, intern_expr thy)
  19.234        (([], Symtab.empty), Expr (Locale target)) |> fst |> fst
  19.235 -      |> List.mapPartial (fn (id, (_, Assumed _)) => SOME id | _ => NONE)
  19.236 +      |> map_filter (fn (id, (_, Assumed _)) => SOME id | _ => NONE)
  19.237  
  19.238      val regs = get_global_registrations thy target;
  19.239  
  19.240 @@ -1598,7 +1597,7 @@
  19.241  
  19.242      val (body, bodyT, body_eq) = atomize_spec thy norm_ts;
  19.243      val env = Term.add_term_free_names (body, []);
  19.244 -    val xs = List.filter (fn (x, _) => x mem_string env) parms;
  19.245 +    val xs = filter (fn (x, _) => x mem_string env) parms;
  19.246      val Ts = map #2 xs;
  19.247      val extraTs = (Term.term_tfrees body \\ foldr Term.add_typ_tfrees [] Ts)
  19.248        |> Library.sort_wrt #1 |> map TFree;
  19.249 @@ -1724,8 +1723,8 @@
  19.250  
  19.251      fun axiomify axioms elemss =
  19.252        (axioms, elemss) |> foldl_map (fn (axs, (id, elems)) => let
  19.253 -                   val ts = List.concat (List.mapPartial (fn (Assumes asms) =>
  19.254 -                     SOME (List.concat (map (map #1 o #2) asms)) | _ => NONE) elems);
  19.255 +                   val ts = flat (map_filter (fn (Assumes asms) =>
  19.256 +                     SOME (maps (map #1 o #2) asms) | _ => NONE) elems);
  19.257                     val (axs1, axs2) = chop (length ts) axs;
  19.258                   in (axs2, ((id, Assumed axs1), elems)) end)
  19.259          |> snd;
  19.260 @@ -1734,7 +1733,7 @@
  19.261        (pred_ctxt, axiomify predicate_axioms elemss');
  19.262      val export = ProofContext.export_view predicate_statement ctxt thy_ctxt;
  19.263      val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])]));
  19.264 -    val elems' = List.concat (map #2 (List.filter (equal "" o #1 o #1) elemss'));
  19.265 +    val elems' = maps #2 (filter (equal "" o #1 o #1) elemss');
  19.266  
  19.267      val thy' = pred_thy
  19.268        |> PureThy.note_thmss_qualified "" bname facts' |> snd
  19.269 @@ -1821,7 +1820,7 @@
  19.270          curry (locale_results kind loc ((names ~~ loc_attss) ~~ loc_results)) loc_ctxt
  19.271          #-> (fn res =>
  19.272            if name = "" andalso null loc_atts then I
  19.273 -          else #2 o locale_results kind loc [((name, loc_atts), List.concat (map #2 res))])
  19.274 +          else #2 o locale_results kind loc [((name, loc_atts), maps #2 res)])
  19.275          #> #2
  19.276          #> after_qed loc_results results
  19.277        end;
  19.278 @@ -1863,7 +1862,7 @@
  19.279  fun extract_asms_elem (Fixes _) ts = ts
  19.280    | extract_asms_elem (Constrains _) ts = ts
  19.281    | extract_asms_elem (Assumes asms) ts =
  19.282 -      ts @ List.concat (map (fn (_, ams) => map (fn (t, _) => t) ams) asms)
  19.283 +      ts @ maps (fn (_, ams) => map (fn (t, _) => t) ams) asms
  19.284    | extract_asms_elem (Defines defs) ts =
  19.285        ts @ map (fn (_, (def, _)) => def) defs
  19.286    | extract_asms_elem (Notes _) ts = ts;
  19.287 @@ -1907,7 +1906,7 @@
  19.288          |> fold (fn (id, thms) => fold (add_wit id) thms)
  19.289             (map fst propss ~~ thmss);
  19.290  
  19.291 -      val prems = List.concat (List.mapPartial
  19.292 +      val prems = flat (map_filter
  19.293              (fn ((id, Assumed _), _) => Option.map snd (get_reg thy_ctxt' id)
  19.294                | ((_, Derived _), _) => NONE) all_elemss);
  19.295        val disch = satisfy_protected prems;
  19.296 @@ -1916,7 +1915,7 @@
  19.297        val thy_ctxt'' = thy_ctxt'
  19.298          (* add witnesses of Derived elements *)
  19.299          |> fold (fn (id, thms) => fold (add_wit id o apsnd disch) thms)
  19.300 -           (List.mapPartial (fn ((_, Assumed _), _) => NONE
  19.301 +           (map_filter (fn ((_, Assumed _), _) => NONE
  19.302                | ((id, Derived thms), _) => SOME (id, thms)) all_elemss)
  19.303      in
  19.304        thy_ctxt''
  19.305 @@ -1963,7 +1962,7 @@
  19.306      val pvTs = map Type.varifyT pTs;
  19.307  
  19.308      (* instantiations given by user *)
  19.309 -    val given = List.mapPartial (fn (_, (NONE, _)) => NONE
  19.310 +    val given = map_filter (fn (_, (NONE, _)) => NONE
  19.311           | (x, (SOME inst, T)) => SOME (x, (inst, T))) (ps ~~ (insts ~~ pvTs));
  19.312      val (given_ps, given_insts) = split_list given;
  19.313      val tvars = foldr Term.add_typ_tvars [] pvTs;
  19.314 @@ -1992,7 +1991,7 @@
  19.315      val inst = Symtab.make (given_ps ~~ map rename vs);
  19.316  
  19.317      (* defined params without user input *)
  19.318 -    val not_given = List.mapPartial (fn (x, (NONE, T)) => SOME (x, T)
  19.319 +    val not_given = map_filter (fn (x, (NONE, T)) => SOME (x, T)
  19.320           | (_, (SOME _, _)) => NONE) (ps ~~ (insts ~~ pTs));
  19.321      fun add_def (p, pT) inst =
  19.322        let
  19.323 @@ -2018,7 +2017,7 @@
  19.324            (Element.inst_term insts t, Element.inst_thm thy insts th))) mode)));
  19.325  
  19.326      (* remove fragments already registered with theory or context *)
  19.327 -    val new_inst_elemss = List.filter (fn ((id, _), _) =>
  19.328 +    val new_inst_elemss = filter (fn ((id, _), _) =>
  19.329            not (test_reg thy_ctxt id)) inst_elemss;
  19.330      val new_ids = map #1 new_inst_elemss;
  19.331  
  19.332 @@ -2072,11 +2071,11 @@
  19.333            the target, unless already present
  19.334          - add facts of induced registrations to theory **)
  19.335  
  19.336 -    val t_ids = List.mapPartial
  19.337 +    val t_ids = map_filter
  19.338          (fn (id, (_, Assumed _)) => SOME id | _ => NONE) target_ids;
  19.339  
  19.340      fun activate thmss thy = let
  19.341 -        val satisfy = satisfy_protected (List.concat thmss);
  19.342 +        val satisfy = satisfy_protected (flat thmss);
  19.343          val ids_elemss_thmss = ids_elemss ~~ thmss;
  19.344          val regs = get_global_registrations thy target;
  19.345  
  19.346 @@ -2090,7 +2089,7 @@
  19.347              fun inst_parms ps = map
  19.348                    (the o AList.lookup (op =) (map #1 fixed ~~ vts)) ps;
  19.349              val disch = satisfy_protected wits;
  19.350 -            val new_elemss = List.filter (fn (((name, ps), _), _) =>
  19.351 +            val new_elemss = filter (fn (((name, ps), _), _) =>
  19.352                  not (test_global_registration thy (name, inst_parms ps))) (ids_elemss);
  19.353              fun activate_assumed_id (((_, Derived _), _), _) thy = thy
  19.354                | activate_assumed_id ((((name, ps), Assumed _), _), thms) thy = let
    20.1 --- a/src/Pure/Isar/method.ML	Thu Apr 27 12:11:56 2006 +0200
    20.2 +++ b/src/Pure/Isar/method.ML	Thu Apr 27 15:06:35 2006 +0200
    20.3 @@ -265,7 +265,7 @@
    20.4    let
    20.5      val rules =
    20.6        if not (null arg_rules) then arg_rules
    20.7 -      else List.concat (ContextRules.find_rules false facts goal ctxt)
    20.8 +      else flat (ContextRules.find_rules false facts goal ctxt)
    20.9    in trace ctxt rules; tac rules facts i end);
   20.10  
   20.11  fun meth tac x = METHOD (HEADGOAL o tac x);
   20.12 @@ -617,7 +617,7 @@
   20.13  local
   20.14  
   20.15  fun sect ss = Scan.first (map Scan.lift ss);
   20.16 -fun thms ss = Scan.repeat (Scan.unless (sect ss) Attrib.multi_thm) >> List.concat;
   20.17 +fun thms ss = Scan.repeat (Scan.unless (sect ss) Attrib.multi_thm) >> flat;
   20.18  
   20.19  fun app (f, att) (context, ths) = foldl_map att (Context.map_proof f context, ths);
   20.20  
    21.1 --- a/src/Pure/Isar/obtain.ML	Thu Apr 27 12:11:56 2006 +0200
    21.2 +++ b/src/Pure/Isar/obtain.ML	Thu Apr 27 15:06:35 2006 +0200
    21.3 @@ -119,7 +119,7 @@
    21.4  
    21.5      (*obtain asms*)
    21.6      val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
    21.7 -    val asm_props = List.concat (map (map fst) proppss);
    21.8 +    val asm_props = maps (map fst) proppss;
    21.9      val asms = map fst (Attrib.map_specs (prep_att thy) raw_asms) ~~ proppss;
   21.10  
   21.11      val _ = ProofContext.warn_extra_tfrees fix_ctxt asms_ctxt;
   21.12 @@ -131,9 +131,9 @@
   21.13      fun occs_var x = Library.get_first (fn t =>
   21.14        Term.find_free t (ProofContext.get_skolem fix_ctxt x)) asm_props;
   21.15      val raw_parms = map occs_var xs;
   21.16 -    val parms = List.mapPartial I raw_parms;
   21.17 +    val parms = map_filter I raw_parms;
   21.18      val parm_names =
   21.19 -      List.mapPartial (fn (SOME (Free a), x) => SOME (a, x) | _ => NONE) (raw_parms ~~ xs);
   21.20 +      map_filter (fn (SOME (Free a), x) => SOME (a, x) | _ => NONE) (raw_parms ~~ xs);
   21.21  
   21.22      val that_name = if name = "" then thatN else name;
   21.23      val that_prop =
   21.24 @@ -284,7 +284,7 @@
   21.25      val names =
   21.26        cases |> map_index (fn (i, ("", _)) => string_of_int (i + 1) | (_, (name, _)) => name);
   21.27      val elems = cases |> map (fn (_, (vars, _)) =>
   21.28 -      Element.Constrains (vars |> List.mapPartial (fn (x, SOME T) => SOME (x, T) | _ => NONE)));
   21.29 +      Element.Constrains (vars |> map_filter (fn (x, SOME T) => SOME (x, T) | _ => NONE)));
   21.30      val concl = cases |> map (fn (_, (_, props)) => (("", []), map (rpair ([], [])) props));
   21.31  
   21.32      fun mk_stmt stmt ctxt =
    22.1 --- a/src/Pure/Isar/outer_parse.ML	Thu Apr 27 12:11:56 2006 +0200
    22.2 +++ b/src/Pure/Isar/outer_parse.ML	Thu Apr 27 15:06:35 2006 +0200
    22.3 @@ -262,11 +262,11 @@
    22.4  val params = Scan.repeat1 name -- Scan.option ($$$ "::" |-- !!! typ)
    22.5    >> (fn (xs, T) => map (rpair T) xs);
    22.6  
    22.7 -val simple_fixes = and_list1 params >> List.concat;
    22.8 +val simple_fixes = and_list1 params >> flat;
    22.9  
   22.10  val fixes =
   22.11    and_list1 (name -- Scan.option ($$$ "::" |-- typ) -- mixfix >> (single o triple1) ||
   22.12 -    params >> map Syntax.no_syn) >> List.concat;
   22.13 +    params >> map Syntax.no_syn) >> flat;
   22.14  
   22.15  
   22.16  (* terms *)
   22.17 @@ -311,7 +311,7 @@
   22.18    ((Scan.repeat1
   22.19      (Scan.repeat1 (atom_arg is_symid blk) ||
   22.20        paren_args "(" ")" (args is_symid) ||
   22.21 -      paren_args "[" "]" (args is_symid))) >> List.concat) x;
   22.22 +      paren_args "[" "]" (args is_symid))) >> flat) x;
   22.23  
   22.24  val arguments = args T.is_sid false;
   22.25  
   22.26 @@ -350,7 +350,7 @@
   22.27  
   22.28  val locale_fixes =
   22.29    and_list1 (name -- Scan.option ($$$ "::" |-- typ) -- locale_mixfix >> (single o triple1) ||
   22.30 -    params >> map Syntax.no_syn) >> List.concat;
   22.31 +    params >> map Syntax.no_syn) >> flat;
   22.32  
   22.33  local
   22.34  
   22.35 @@ -401,7 +401,7 @@
   22.36  
   22.37  val obtain_case =
   22.38    parname -- (Scan.optional (simple_fixes --| $$$ "where") [] --
   22.39 -    (and_list1 (Scan.repeat1 prop) >> List.concat));
   22.40 +    (and_list1 (Scan.repeat1 prop) >> flat));
   22.41  
   22.42  val general_statement =
   22.43    statement >> (fn x => ([], Element.Shows x)) ||
    23.1 --- a/src/Pure/Isar/outer_syntax.ML	Thu Apr 27 12:11:56 2006 +0200
    23.2 +++ b/src/Pure/Isar/outer_syntax.ML	Thu Apr 27 15:06:35 2006 +0200
    23.3 @@ -197,10 +197,10 @@
    23.4      |> Source.source T.stopper
    23.5        (Scan.bulk (P.$$$ "--" -- P.!!! P.text >> K NONE || P.not_eof >> SOME))
    23.6        (if do_recover then SOME recover else NONE)
    23.7 -    |> Source.mapfilter I
    23.8 +    |> Source.map_filter I
    23.9      |> Source.source T.stopper (Scan.bulk (fn xs => P.!!! (command term do_trace (cmd ())) xs))
   23.10        (if do_recover then SOME recover else NONE)
   23.11 -    |> Source.mapfilter I
   23.12 +    |> Source.map_filter I
   23.13    end;
   23.14  
   23.15  
    24.1 --- a/src/Pure/Isar/proof.ML	Thu Apr 27 12:11:56 2006 +0200
    24.2 +++ b/src/Pure/Isar/proof.ML	Thu Apr 27 15:06:35 2006 +0200
    24.3 @@ -237,7 +237,7 @@
    24.4    put_thms_internal (AutoBind.thisN, facts);
    24.5  
    24.6  fun these_factss more_facts (named_factss, state) =
    24.7 -  (named_factss, state |> put_facts (SOME (List.concat (map snd named_factss) @ more_facts)));
    24.8 +  (named_factss, state |> put_facts (SOME (maps snd named_factss @ more_facts)));
    24.9  
   24.10  fun export_facts inner outer =
   24.11    (case get_facts inner of
   24.12 @@ -655,7 +655,7 @@
   24.13      state' |> map_goal I (fn (statement, using, goal, before_qed, after_qed) =>
   24.14        let
   24.15          val ctxt = context_of state';
   24.16 -        val ths = List.concat (map snd named_facts);
   24.17 +        val ths = maps snd named_facts;
   24.18        in (statement, f ctxt ths using, g ctxt ths goal, before_qed, after_qed) end));
   24.19  
   24.20  fun append_using _ ths using = using @ ths;
   24.21 @@ -794,7 +794,7 @@
   24.22        |> enter_forward
   24.23        |> open_block
   24.24        |> map_context_result (fn ctxt => swap (prepp (ctxt, raw_propp)));
   24.25 -    val props = List.concat propss;
   24.26 +    val props = flat propss;
   24.27  
   24.28      val goal = Goal.init (Thm.cterm_of thy (Logic.mk_conjunction_list2 propss));
   24.29      val after_qed' = after_qed |>> (fn after_local =>
   24.30 @@ -823,7 +823,7 @@
   24.31      val outer_ctxt = context_of outer_state;
   24.32  
   24.33      val props =
   24.34 -      List.concat stmt
   24.35 +      flat stmt
   24.36        |> ProofContext.generalize goal_ctxt outer_ctxt;
   24.37      val results =
   24.38        stmt
   24.39 @@ -874,7 +874,7 @@
   24.40        #> global_results kind ((names ~~ attss) ~~ res)
   24.41        #-> (fn res' =>
   24.42          (print_results thy_ctxt ((kind, name), res') : unit;
   24.43 -          #2 o global_results kind [((name, atts), List.concat (map #2 res'))]))
   24.44 +          #2 o global_results kind [((name, atts), maps #2 res')]))
   24.45        #> Sign.restore_naming thy;
   24.46  
   24.47      fun after_qed' results =
   24.48 @@ -961,7 +961,7 @@
   24.49        |> capture;
   24.50  
   24.51      fun after_qed' results =
   24.52 -      refine_goals print_rule (context_of state) (List.concat results)
   24.53 +      refine_goals print_rule (context_of state) (flat results)
   24.54        #> Seq.maps (after_qed results);
   24.55    in
   24.56      state
    25.1 --- a/src/Pure/Isar/proof_context.ML	Thu Apr 27 12:11:56 2006 +0200
    25.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Apr 27 15:06:35 2006 +0200
    25.3 @@ -280,8 +280,8 @@
    25.4  val fixed_names_of = map #2 o fixes_of;
    25.5  
    25.6  val assumptions_of = #1 o #assms o rep_context;
    25.7 -val assms_of = map Thm.term_of o List.concat o map #1 o assumptions_of;
    25.8 -val prems_of = List.concat o map #2 o #2 o #assms o rep_context;
    25.9 +val assms_of = map Thm.term_of o maps #1 o assumptions_of;
   25.10 +val prems_of = maps #2 o #2 o #assms o rep_context;
   25.11  
   25.12  val binds_of = #binds o rep_context;
   25.13  
   25.14 @@ -778,7 +778,7 @@
   25.15        let
   25.16          val thy = Thm.theory_of_thm rule;
   25.17          val prop = Thm.full_prop_of rule;
   25.18 -        val frees = map (Thm.cterm_of thy) (List.mapPartial (Term.find_free prop) fixes);
   25.19 +        val frees = map (Thm.cterm_of thy) (map_filter (Term.find_free prop) fixes);
   25.20          val tfrees = gen (Term.add_term_tfree_names (prop, []));
   25.21        in
   25.22          rule
   25.23 @@ -849,7 +849,7 @@
   25.24            then () else fail ();
   25.25          fun norm_bind (xi, (_, t)) =
   25.26            if member (op =) domain xi then SOME (xi, Envir.norm_term env t) else NONE;
   25.27 -      in List.mapPartial norm_bind (Envir.alist_of env) end;
   25.28 +      in map_filter norm_bind (Envir.alist_of env) end;
   25.29  
   25.30  
   25.31  (* add_binds(_i) *)
   25.32 @@ -889,7 +889,7 @@
   25.33    let
   25.34      val ts = prep_terms ctxt (map snd raw_binds);
   25.35      val (binds, ctxt') =
   25.36 -      apfst List.concat (fold_map (prep_bind prep_pats) (map fst raw_binds ~~ ts) ctxt);
   25.37 +      apfst flat (fold_map (prep_bind prep_pats) (map fst raw_binds ~~ ts) ctxt);
   25.38      val binds' =
   25.39        if gen then map #1 binds ~~ generalize ctxt' ctxt (map #2 binds)
   25.40        else binds;
   25.41 @@ -922,7 +922,7 @@
   25.42            in ((prop, chop (length raw_pats1) pats), (ctxt', props)) end
   25.43        | prep _ _ = sys_error "prep_propp";
   25.44      val (propp, (context', _)) = (fold_map o fold_map) prep args
   25.45 -      (context, prep_props schematic context (List.concat (map (map fst) args)));
   25.46 +      (context, prep_props schematic context (maps (map fst) args));
   25.47    in (context', propp) end;
   25.48  
   25.49  fun matches ctxt (prop, (pats1, pats2)) =
   25.50 @@ -931,7 +931,7 @@
   25.51  fun gen_bind_propp prepp (ctxt, raw_args) =
   25.52    let
   25.53      val (ctxt', args) = prepp (ctxt, raw_args);
   25.54 -    val binds = List.concat (List.concat (map (map (matches ctxt')) args));
   25.55 +    val binds = flat (flat (map (map (matches ctxt')) args));
   25.56      val propss = map (map #1) args;
   25.57  
   25.58      (*generalize result: context evaluated now, binds added later*)
   25.59 @@ -1061,7 +1061,7 @@
   25.60        let val (ct', th') = foldl_map (Thm.proof_attributes (attrs @ more_attrs)) (ct, get ctxt th)
   25.61        in (ct', th' :: ths) end;
   25.62      val (ctxt', rev_thms) = fold app ths_attrs (ctxt, []);
   25.63 -    val thms = List.concat (rev rev_thms);
   25.64 +    val thms = flat (rev rev_thms);
   25.65    in ((name, thms), ctxt' |> put_thms true (name, SOME thms)) end);
   25.66  
   25.67  in
   25.68 @@ -1245,7 +1245,7 @@
   25.69      val (propss, ctxt1) = swap (prepp (ctxt, map snd args));
   25.70      val (results, ctxt2) = fold_map gen_assm (map fst args ~~ propss) ctxt1;
   25.71  
   25.72 -    val new_asms = List.concat (map #1 results);
   25.73 +    val new_asms = maps #1 results;
   25.74      val new_prems = map #2 results;
   25.75      val ctxt3 = ctxt2
   25.76        |> map_assms (fn (asms, prems) => (asms @ [(new_asms, exp)], prems @ new_prems))
   25.77 @@ -1428,13 +1428,13 @@
   25.78  
   25.79      fun prt_sect _ _ _ [] = []
   25.80        | prt_sect s sep prt xs = [Pretty.block (Pretty.breaks (Pretty.str s ::
   25.81 -            List.concat (Library.separate sep (map (Library.single o prt) xs))))];
   25.82 +            flat (Library.separate sep (map (Library.single o prt) xs))))];
   25.83  
   25.84      fun prt_case (name, (fixes, (asms, (lets, cs)))) = Pretty.block (Pretty.fbreaks
   25.85        (Pretty.str (name ^ ":") ::
   25.86          prt_sect "fix" [] (Pretty.str o fst) fixes @
   25.87          prt_sect "let" [Pretty.str "and"] prt_let
   25.88 -          (List.mapPartial (fn (xi, SOME t) => SOME (xi, t) | _ => NONE) lets) @
   25.89 +          (map_filter (fn (xi, SOME t) => SOME (xi, t) | _ => NONE) lets) @
   25.90          (if forall (null o #2) asms then []
   25.91            else prt_sect "assume" [Pretty.str "and"] prt_asm asms) @
   25.92          prt_sect "subcases:" [] (Pretty.str o fst) cs));
    26.1 --- a/src/Pure/Isar/proof_display.ML	Thu Apr 27 12:11:56 2006 +0200
    26.2 +++ b/src/Pure/Isar/proof_display.ML	Thu Apr 27 15:06:35 2006 +0200
    26.3 @@ -62,7 +62,7 @@
    26.4  local
    26.5  
    26.6  fun pretty_facts ctxt =
    26.7 -  List.concat o (separate [Pretty.fbrk, Pretty.str "and "]) o
    26.8 +  flat o (separate [Pretty.fbrk, Pretty.str "and "]) o
    26.9      map (single o ProofContext.pretty_fact ctxt);
   26.10  
   26.11  fun pretty_results ctxt ((kind, ""), facts) =
   26.12 @@ -76,7 +76,7 @@
   26.13  fun name_results "" res = res
   26.14    | name_results name res =
   26.15        let
   26.16 -        val n = length (List.concat (map snd res));
   26.17 +        val n = length (maps snd res);
   26.18          fun name_res (a, ths) i =
   26.19            let
   26.20              val m = length ths;
    27.1 --- a/src/Pure/Isar/rule_cases.ML	Thu Apr 27 12:11:56 2006 +0200
    27.2 +++ b/src/Pure/Isar/rule_cases.ML	Thu Apr 27 15:06:35 2006 +0200
    27.3 @@ -107,7 +107,7 @@
    27.4            else abs fixes1 (app (map (Term.dummy_pattern o #2) fixes2) (abs fixes2 t));
    27.5  
    27.6          val (assumes1, assumes2) = extract_assumes (NameSpace.qualified name) case_outline prop
    27.7 -          |> pairself (map (apsnd (List.concat o map Logic.dest_conjunctions)));
    27.8 +          |> pairself (map (apsnd (maps Logic.dest_conjunctions)));
    27.9  
   27.10          val concl = ObjectLogic.drop_judgment thy (Logic.strip_assums_concl prop);
   27.11          val binds =
   27.12 @@ -272,7 +272,7 @@
   27.13    | _ => []);
   27.14  
   27.15  fun save_case_concls th =
   27.16 -  let val concls = Thm.tags_of_thm th |> List.mapPartial
   27.17 +  let val concls = Thm.tags_of_thm th |> map_filter
   27.18      (fn (a, b :: cs) =>
   27.19        if a = case_concl_tagN then SOME (b, cs) else NONE
   27.20      | _ => NONE)
    28.1 --- a/src/Pure/Proof/extraction.ML	Thu Apr 27 12:11:56 2006 +0200
    28.2 +++ b/src/Pure/Proof/extraction.ML	Thu Apr 27 15:06:35 2006 +0200
    28.3 @@ -307,7 +307,7 @@
    28.4    let
    28.5      val {realizes_eqns, typeof_eqns, defs, types, ...} =
    28.6        ExtractionData.get thy;
    28.7 -    val procs = List.concat (map (fst o snd) types);
    28.8 +    val procs = maps (fst o snd) types;
    28.9      val rtypes = map fst types;
   28.10      val eqns = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
   28.11      val thy' = add_syntax thy;
   28.12 @@ -343,7 +343,7 @@
   28.13      val thy' = add_syntax thy;
   28.14      val {realizes_eqns, typeof_eqns, defs, types, ...} =
   28.15        ExtractionData.get thy';
   28.16 -    val procs = List.concat (map (fst o snd) types);
   28.17 +    val procs = maps (fst o snd) types;
   28.18      val eqns = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
   28.19      val prop' = Pattern.rewrite_term thy'
   28.20        (map (Logic.dest_equals o prop_of) defs) [] prop;
   28.21 @@ -460,7 +460,7 @@
   28.22      val thy' = add_syntax thy;
   28.23      val {realizes_eqns, typeof_eqns, types, realizers, defs, expand, prep} =
   28.24        ExtractionData.get thy;
   28.25 -    val procs = List.concat (map (fst o snd) types);
   28.26 +    val procs = maps (fst o snd) types;
   28.27      val rtypes = map fst types;
   28.28      val typroc = typeof_proc (Sign.defaultS thy');
   28.29      val prep = the_default (K I) prep thy' o ProofRewriteRules.elim_defs thy' false defs o
    29.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Thu Apr 27 12:11:56 2006 +0200
    29.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Thu Apr 27 15:06:35 2006 +0200
    29.3 @@ -246,11 +246,11 @@
    29.4      val f = if not r then I else
    29.5        let
    29.6          val cnames = map (fst o dest_Const o fst) defs';
    29.7 -        val thms = List.concat (map (fn (s, ps) =>
    29.8 +        val thms = maps (fn (s, ps) =>
    29.9              if s mem defnames then []
   29.10              else map (pair s o SOME o fst) (filter_out (fn (p, _) =>
   29.11                null (term_consts p inter cnames)) ps))
   29.12 -          (Symtab.dest (thms_of_proof prf Symtab.empty)))
   29.13 +          (Symtab.dest (thms_of_proof prf Symtab.empty))
   29.14        in Reconstruct.expand_proof thy thms end
   29.15    in
   29.16      rewrite_terms (Pattern.rewrite_term thy defs' [])
    30.1 --- a/src/Pure/Proof/reconstruct.ML	Thu Apr 27 12:11:56 2006 +0200
    30.2 +++ b/src/Pure/Proof/reconstruct.ML	Thu Apr 27 15:06:35 2006 +0200
    30.3 @@ -110,7 +110,7 @@
    30.4  
    30.5  fun decompose sg Ts (env, p as (t, u)) =
    30.6    let fun rigrig (a, T) (b, U) uT ts us = if a <> b then cantunify sg p
    30.7 -    else apsnd List.concat (foldl_map (decompose sg Ts) (uT env T U, ts ~~ us))
    30.8 +    else apsnd flat (foldl_map (decompose sg Ts) (uT env T U, ts ~~ us))
    30.9    in case pairself (strip_comb o Envir.head_norm env) p of
   30.10        ((Const c, ts), (Const d, us)) => rigrig c d (unifyT sg) ts us
   30.11      | ((Free c, ts), (Free d, us)) => rigrig c d (unifyT sg) ts us
    31.1 --- a/src/Pure/Syntax/lexicon.ML	Thu Apr 27 12:11:56 2006 +0200
    31.2 +++ b/src/Pure/Syntax/lexicon.ML	Thu Apr 27 15:06:35 2006 +0200
    31.3 @@ -279,7 +279,7 @@
    31.4        Scan.one Symbol.is_blank >> K NONE;
    31.5    in
    31.6      (case Scan.error (Scan.finite Symbol.stopper (Scan.repeat scan_token)) chs of
    31.7 -      (toks, []) => List.mapPartial I toks @ [EndToken]
    31.8 +      (toks, []) => map_filter I toks @ [EndToken]
    31.9      | (_, cs) => error ("Inner lexical error at: " ^ quote (implode cs)))
   31.10    end;
   31.11  
    32.1 --- a/src/Pure/Syntax/mixfix.ML	Thu Apr 27 12:11:56 2006 +0200
    32.2 +++ b/src/Pure/Syntax/mixfix.ML	Thu Apr 27 15:06:35 2006 +0200
    32.3 @@ -183,7 +183,7 @@
    32.4          | _ => error ("Bad mixfix declaration for type: " ^ quote t))
    32.5        end;
    32.6  
    32.7 -    val mfix = List.mapPartial mfix_of type_decls;
    32.8 +    val mfix = map_filter mfix_of type_decls;
    32.9      val xconsts = map name_of type_decls;
   32.10    in SynExt.syn_ext mfix xconsts ([], [], [], []) [] ([], []) end;
   32.11  
   32.12 @@ -224,9 +224,9 @@
   32.13      fun binder (c, _, Binder (sy, _, _)) = SOME (sy, c)
   32.14        | binder _ = NONE;
   32.15  
   32.16 -    val mfix = List.concat (map mfix_of const_decls);
   32.17 +    val mfix = maps mfix_of const_decls;
   32.18      val xconsts = map name_of const_decls;
   32.19 -    val binders = List.mapPartial binder const_decls;
   32.20 +    val binders = map_filter binder const_decls;
   32.21      val binder_trs = binders |> map (SynExt.stamp_trfun binder_stamp o
   32.22          apsnd K o SynTrans.mk_binder_tr);
   32.23      val binder_trs' = binders |> map (SynExt.stamp_trfun binder_stamp o
    33.1 --- a/src/Pure/Syntax/parser.ML	Thu Apr 27 12:11:56 2006 +0200
    33.2 +++ b/src/Pure/Syntax/parser.ML	Thu Apr 27 15:06:35 2006 +0200
    33.3 @@ -418,7 +418,7 @@
    33.4            map prod_of_chain ((these o AList.lookup (op =) chains) tag);
    33.5        in map (pretty_prod name) nt_prods end;
    33.6  
    33.7 -  in List.concat (map pretty_nt taglist) end;
    33.8 +  in maps pretty_nt taglist end;
    33.9  
   33.10  
   33.11  (** Operations on gramars **)
   33.12 @@ -840,12 +840,12 @@
   33.13                    end;
   33.14  
   33.15                val nts =
   33.16 -                List.mapPartial (fn (_, _, _, Nonterminal (a, prec) :: _, _, _) =>
   33.17 +                map_filter (fn (_, _, _, Nonterminal (a, prec) :: _, _, _) =>
   33.18                             SOME (a, prec) | _ => NONE)
   33.19                            (Array.sub (stateset, i-1));
   33.20                val allowed =
   33.21                  distinct (op =) (get_starts nts [] @
   33.22 -                  (List.mapPartial (fn (_, _, _, Terminal a :: _, _, _) => SOME a
   33.23 +                  (map_filter (fn (_, _, _, Terminal a :: _, _, _) => SOME a
   33.24                                 | _ => NONE)
   33.25                               (Array.sub (stateset, i-1))));
   33.26            in syntax_error (if prev_token = EndToken then indata
   33.27 @@ -862,7 +862,7 @@
   33.28         end));
   33.29  
   33.30  
   33.31 -fun get_trees l = List.mapPartial (fn (_, _, [pt], _, _, _) => SOME pt | _ => NONE)
   33.32 +fun get_trees l = map_filter (fn (_, _, [pt], _, _, _) => SOME pt | _ => NONE)
   33.33                              l;
   33.34  
   33.35  fun earley prods tags chains startsymbol indata =
    34.1 --- a/src/Pure/Syntax/printer.ML	Thu Apr 27 12:11:56 2006 +0200
    34.2 +++ b/src/Pure/Syntax/printer.ML	Thu Apr 27 15:06:35 2006 +0200
    34.3 @@ -192,7 +192,7 @@
    34.4  type prtabs = (string * ((symb list * int * int) list) Symtab.table) list;
    34.5  
    34.6  fun mode_tab prtabs mode = the_default Symtab.empty (AList.lookup (op =) prtabs mode);
    34.7 -fun mode_tabs prtabs modes = List.mapPartial (AList.lookup (op =) prtabs) (modes @ [""]);
    34.8 +fun mode_tabs prtabs modes = map_filter (AList.lookup (op =) prtabs) (modes @ [""]);
    34.9  
   34.10  
   34.11  (* xprod_to_fmt *)
   34.12 @@ -244,7 +244,7 @@
   34.13  
   34.14  fun change_prtabs f mode xprods prtabs =
   34.15    let
   34.16 -    val fmts = List.mapPartial xprod_to_fmt xprods;
   34.17 +    val fmts = map_filter xprod_to_fmt xprods;
   34.18      val tab = fold f fmts (mode_tab prtabs mode);
   34.19    in AList.update (op =) (mode, tab) prtabs end;
   34.20  
    35.1 --- a/src/Pure/Syntax/syn_ext.ML	Thu Apr 27 12:11:56 2006 +0200
    35.2 +++ b/src/Pure/Syntax/syn_ext.ML	Thu Apr 27 15:06:35 2006 +0200
    35.3 @@ -218,7 +218,7 @@
    35.4    $$ "'" -- Scan.one Symbol.is_blank >> K NONE;
    35.5  
    35.6  val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (~$$ "'");
    35.7 -val read_symbs = List.mapPartial I o the o Scan.read Symbol.stopper scan_symbs;
    35.8 +val read_symbs = map_filter I o the o Scan.read Symbol.stopper scan_symbs;
    35.9  
   35.10  fun unique_index xsymbs =
   35.11    if length (List.filter is_index xsymbs) <= 1 then xsymbs
   35.12 @@ -360,7 +360,7 @@
   35.13        print_ast_translation) = trfuns;
   35.14  
   35.15      val (xprods, parse_rules') = map (mfix_to_xprod convert is_logtype) mfixes
   35.16 -      |> split_list |> apsnd (rev o List.concat);
   35.17 +      |> split_list |> apsnd (rev o flat);
   35.18      val mfix_consts =
   35.19        distinct (op =) (map (fn Mfix x => #3 x) mfixes @ map (fn XProd x => #3 x) xprods);
   35.20    in
    36.1 --- a/src/Pure/Syntax/syn_trans.ML	Thu Apr 27 12:11:56 2006 +0200
    36.2 +++ b/src/Pure/Syntax/syn_trans.ML	Thu Apr 27 15:06:35 2006 +0200
    36.3 @@ -467,8 +467,8 @@
    36.4        | ast_of (Parser.Tip tok) = Ast.Variable (Lexicon.str_of_token tok);
    36.5  
    36.6      val exn_results = map (capture ast_of) pts;
    36.7 -    val exns = List.mapPartial get_exn exn_results;
    36.8 -    val results = List.mapPartial get_result exn_results
    36.9 +    val exns = map_filter get_exn exn_results;
   36.10 +    val results = map_filter get_result exn_results
   36.11    in (case (results, exns) of ([], exn :: _) => raise exn | _ => results) end;
   36.12  
   36.13  
   36.14 @@ -500,8 +500,8 @@
   36.15          | t => t);
   36.16  
   36.17      val exn_results = map (capture (term_of #> free_fixed)) asts;
   36.18 -    val exns = List.mapPartial get_exn exn_results;
   36.19 -    val results = List.mapPartial get_result exn_results
   36.20 +    val exns = map_filter get_exn exn_results;
   36.21 +    val results = map_filter get_result exn_results
   36.22    in (case (results, exns) of ([], exn :: _) => raise exn | _ => results) end;
   36.23  
   36.24  end;
    37.1 --- a/src/Pure/Syntax/syntax.ML	Thu Apr 27 12:11:56 2006 +0200
    37.2 +++ b/src/Pure/Syntax/syntax.ML	Thu Apr 27 15:06:35 2006 +0200
    37.3 @@ -114,8 +114,7 @@
    37.4  (** tables of token translation functions **)
    37.5  
    37.6  fun lookup_tokentr tabs modes =
    37.7 -  let val trs = distinct (eq_fst (op =))
    37.8 -    (List.concat (map (these o AList.lookup (op =) tabs) (modes @ [""])))
    37.9 +  let val trs = distinct (eq_fst (op =)) (maps (these o AList.lookup (op =) tabs) (modes @ [""]))
   37.10    in fn c => Option.map fst (AList.lookup (op =) trs c) end;
   37.11  
   37.12  fun merge_tokentrtabs tabs1 tabs2 =
   37.13 @@ -150,7 +149,7 @@
   37.14  
   37.15  type ruletab = (Ast.ast * Ast.ast) list Symtab.table;
   37.16  
   37.17 -fun dest_ruletab tab = List.concat (map snd (Symtab.dest tab));
   37.18 +fun dest_ruletab tab = maps snd (Symtab.dest tab);
   37.19  
   37.20  
   37.21  (* empty, extend, merge ruletabs *)
   37.22 @@ -474,8 +473,8 @@
   37.23  
   37.24  fun prep_rules rd_pat raw_rules =
   37.25    let val rules = map (map_trrule rd_pat) raw_rules in
   37.26 -    (map check_rule (List.mapPartial parse_rule rules),
   37.27 -      map check_rule (List.mapPartial print_rule rules))
   37.28 +    (map check_rule (map_filter parse_rule rules),
   37.29 +      map check_rule (map_filter print_rule rules))
   37.30    end
   37.31  
   37.32  in
    38.1 --- a/src/Pure/Thy/thm_database.ML	Thu Apr 27 12:11:56 2006 +0200
    38.2 +++ b/src/Pure/Thy/thm_database.ML	Thu Apr 27 15:06:35 2006 +0200
    38.3 @@ -104,7 +104,7 @@
    38.4      fun mk_thm (bname, xname, singleton) =
    38.5        "val " ^ bname ^ " = thm" ^ (if singleton then "" else "s") ^ " " ^ quote xname;
    38.6    in
    38.7 -    Symtab.keys thms |> List.mapPartial prune
    38.8 +    Symtab.keys thms |> map_filter prune
    38.9      |> Symtab.make_list |> Symtab.dest |> sort_wrt #1
   38.10      |> map (fn (prfx, entries) =>
   38.11        entries |> sort_wrt #1 |> map mk_thm |> cat_lines |> mk_struct prfx)
    39.1 --- a/src/Pure/Thy/thy_info.ML	Thu Apr 27 12:11:56 2006 +0200
    39.2 +++ b/src/Pure/Thy/thy_info.ML	Thu Apr 27 15:06:35 2006 +0200
    39.3 @@ -157,7 +157,7 @@
    39.4      NONE => []
    39.5    | SOME {master, files, ...} =>
    39.6        (case master of SOME m => [#1 (ThyLoad.get_thy m)] | NONE => []) @
    39.7 -      (List.mapPartial (Option.map #1 o #2) files));
    39.8 +      (map_filter (Option.map #1 o #2) files));
    39.9  
   39.10  fun get_preds name =
   39.11    (thy_graph Graph.imm_preds name) handle Graph.UNDEF _ =>
   39.12 @@ -222,7 +222,7 @@
   39.13  in
   39.14  
   39.15  fun touch_thys names =
   39.16 -  List.app outdate_thy (thy_graph Graph.all_succs (List.mapPartial check_unfinished names));
   39.17 +  List.app outdate_thy (thy_graph Graph.all_succs (map_filter check_unfinished names));
   39.18  
   39.19  fun touch_thy name = touch_thys [name];
   39.20  fun touch_child_thys name = touch_thys (thy_graph Graph.imm_succs name);
   39.21 @@ -298,7 +298,7 @@
   39.22        else #1 (ThyLoad.deps_thy dir name ml);
   39.23  
   39.24      val files = get_files name;
   39.25 -    val missing_files = List.mapPartial (fn (path, NONE) => SOME (Path.pack path) | _ => NONE) files;
   39.26 +    val missing_files = map_filter (fn (path, NONE) => SOME (Path.pack path) | _ => NONE) files;
   39.27    in
   39.28      if null missing_files then ()
   39.29      else warning (loader_msg "unresolved dependencies of theory" [name] ^
   39.30 @@ -434,7 +434,7 @@
   39.31      val deps =
   39.32        if known_thy name then get_deps name
   39.33        else (init_deps NONE (map #1 uses));   (*records additional ML files only!*)
   39.34 -    val uses_now = List.mapPartial (fn (x, true) => SOME x | _ => NONE) uses;
   39.35 +    val uses_now = map_filter (fn (x, true) => SOME x | _ => NONE) uses;
   39.36  
   39.37      val _ = change_thys (update_node name bparents (deps, SOME (Theory.copy theory)));
   39.38      val theory' = theory |> present dir' name bparents uses;
   39.39 @@ -470,7 +470,7 @@
   39.40      fun get_variant (x, y_name) =
   39.41        if Theory.eq_thy (x, get_theory y_name) then NONE
   39.42        else SOME y_name;
   39.43 -    val variants = List.mapPartial get_variant (parents ~~ parent_names);
   39.44 +    val variants = map_filter get_variant (parents ~~ parent_names);
   39.45  
   39.46      fun register G =
   39.47        (Graph.new_node (name, (NONE, SOME theory)) G
    40.1 --- a/src/Pure/Tools/am_compiler.ML	Thu Apr 27 12:11:56 2006 +0200
    40.2 +++ b/src/Pure/Tools/am_compiler.ML	Thu Apr 27 15:06:35 2006 +0200
    40.3 @@ -113,7 +113,7 @@
    40.4    | remove_dups [] = []
    40.5  
    40.6  fun constants_of PVar = []
    40.7 -  | constants_of (PConst (c, ps)) = c :: List.concat (map constants_of ps)
    40.8 +  | constants_of (PConst (c, ps)) = c :: maps constants_of ps
    40.9  
   40.10  fun constants_of_term (Var _) = []
   40.11    | constants_of_term (Abs m) = constants_of_term m
   40.12 @@ -133,7 +133,7 @@
   40.13  		"structure "^name^" = struct",
   40.14  		"",
   40.15  		"datatype term = App of term * term | Abs of term | Var of int | Const of int | Closure of term list * term"]
   40.16 -	val constants = remove_dups (List.concat (map (fn (p, r) => ((constants_of p)@(constants_of_term r))) prog))
   40.17 +	val constants = remove_dups (maps (fn (p, r) => ((constants_of p)@(constants_of_term r))) prog)
   40.18  	val _ = map (fn x => write (" | c"^(str x))) constants
   40.19  	val _ = writelist [
   40.20  		"",
    41.1 --- a/src/Pure/Tools/class_package.ML	Thu Apr 27 12:11:56 2006 +0200
    41.2 +++ b/src/Pure/Tools/class_package.ML	Thu Apr 27 15:06:35 2006 +0200
    41.3 @@ -177,7 +177,7 @@
    41.4  fun the_intros thy =
    41.5    let
    41.6      val gr = (fst o fst o ClassData.get) thy;
    41.7 -  in (List.mapPartial (#intro o rep_classdata o Graph.get_node gr) o Graph.keys) gr end;
    41.8 +  in (map_filter (#intro o rep_classdata o Graph.get_node gr) o Graph.keys) gr end;
    41.9  
   41.10  fun subst_clsvar v ty_subst =
   41.11    map_type_tfree (fn u as (w, _) =>
    42.1 --- a/src/Pure/Tools/codegen_package.ML	Thu Apr 27 12:11:56 2006 +0200
    42.2 +++ b/src/Pure/Tools/codegen_package.ML	Thu Apr 27 15:06:35 2006 +0200
    42.3 @@ -164,14 +164,14 @@
    42.4                  NameSpace.drop_base c';
    42.5        val c'' = NameSpace.append prefix (NameSpace.base c');
    42.6        fun mangle (Type (tyco, tys)) =
    42.7 -            (NameSpace.base o alias_get thy) tyco :: flat (List.mapPartial mangle tys) |> SOME
    42.8 +            (NameSpace.base o alias_get thy) tyco :: flat (map_filter mangle tys) |> SOME
    42.9          | mangle _ =
   42.10              NONE
   42.11      in
   42.12        Vartab.empty
   42.13        |> Type.raw_match (Sign.the_const_type thy c, ty)
   42.14        |> map (snd o snd) o Vartab.dest
   42.15 -      |> List.mapPartial mangle
   42.16 +      |> map_filter mangle
   42.17        |> flat
   42.18        |> null ? K ["x"]
   42.19        |> cons c''
    43.1 --- a/src/Pure/Tools/codegen_serializer.ML	Thu Apr 27 12:11:56 2006 +0200
    43.2 +++ b/src/Pure/Tools/codegen_serializer.ML	Thu Apr 27 15:06:35 2006 +0200
    43.3 @@ -322,7 +322,7 @@
    43.4        then SOME eq
    43.5        else (warning ("in function " ^ quote name ^ ", throwing away one "
    43.6          ^ "non-executable function clause"); NONE)
    43.7 -  in case List.mapPartial check_eq eqs
    43.8 +  in case map_filter check_eq eqs
    43.9     of [] => error ("in function " ^ quote name ^ ", no"
   43.10          ^ "executable function clauses found")
   43.11      | eqs => (name, (eqs, ty))
   43.12 @@ -666,13 +666,13 @@
   43.13      val (ml_from_funs, ml_from_datatypes) =
   43.14        ml_fun_datatyp (is_cons, needs_type) (tyco_syntax, const_syntax) resolv;
   43.15      val filter_datatype =
   43.16 -      List.mapPartial
   43.17 +      map_filter
   43.18          (fn (name, CodegenThingol.Datatype info) => SOME (name, info)
   43.19            | (name, CodegenThingol.Datatypecons _) => NONE
   43.20            | (name, def) => error ("datatype block containing illegal def: "
   43.21                  ^ (Pretty.output o CodegenThingol.pretty_def) def));
   43.22      fun filter_class defs = 
   43.23 -      case List.mapPartial
   43.24 +      case map_filter
   43.25          (fn (name, CodegenThingol.Class info) => SOME (name, info)
   43.26            | (name, CodegenThingol.Classmember _) => NONE
   43.27            | (name, def) => error ("class block containing illegal def: "
   43.28 @@ -1085,7 +1085,7 @@
   43.29        | hs_from_def (_, CodegenThingol.Classinstmember) =
   43.30            NONE
   43.31    in
   43.32 -    case List.mapPartial (fn (name, def) => hs_from_def (name, def)) defs
   43.33 +    case map_filter (fn (name, def) => hs_from_def (name, def)) defs
   43.34       of [] => NONE
   43.35        | l => (SOME o Pretty.chunks o separate (str "")) l
   43.36    end;
    44.1 --- a/src/Pure/Tools/codegen_theorems.ML	Thu Apr 27 12:11:56 2006 +0200
    44.2 +++ b/src/Pure/Tools/codegen_theorems.ML	Thu Apr 27 15:06:35 2006 +0200
    44.3 @@ -429,7 +429,7 @@
    44.4  
    44.5  fun get_funs thy (c, ty) =
    44.6    let
    44.7 -    val filter_typ = Library.mapfilter (fn ((_, ty'), thm) =>
    44.8 +    val filter_typ = map_filter (fn ((_, ty'), thm) =>
    44.9        if Sign.typ_instance thy (ty', ty)
   44.10          orelse Sign.typ_instance thy (ty, ty')
   44.11        then SOME thm else debug_msg (fn _ => "dropping " ^ string_of_thm thm) NONE);
    45.1 --- a/src/Pure/Tools/codegen_thingol.ML	Thu Apr 27 12:11:56 2006 +0200
    45.2 +++ b/src/Pure/Tools/codegen_thingol.ML	Thu Apr 27 15:06:35 2006 +0200
    45.3 @@ -503,7 +503,7 @@
    45.4              Pretty.str ("module " ^ name ^ " {")
    45.5              :: Pretty.brk 1
    45.6              :: Pretty.chunks (map pretty (AList.make (Graph.get_node modl)
    45.7 -                 (Graph.strong_conn modl |> List.concat |> rev)))
    45.8 +                 (Graph.strong_conn modl |> flat |> rev)))
    45.9              :: Pretty.str "}" :: nil
   45.10            )
   45.11        | pretty (name, Def def) =
   45.12 @@ -533,7 +533,7 @@
   45.13    in
   45.14      modl
   45.15      |> Graph.strong_conn
   45.16 -    |> List.concat
   45.17 +    |> flat
   45.18      |> rev
   45.19      |> map one_node
   45.20      |> Pretty.chunks
   45.21 @@ -1121,7 +1121,7 @@
   45.22          val name_qual = NameSpace.pack (prfx @ [name])
   45.23        in (name_qual, resolver prfx name_qual) end;
   45.24      fun mk_contents prfx module =
   45.25 -      List.mapPartial (seri prfx)
   45.26 +      map_filter (seri prfx)
   45.27          ((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module)
   45.28      and seri prfx ([(name, Module modl)]) =
   45.29            seri_module (resolver []) (map (resolver []) (imports_of module (prfx @ [name])))
   45.30 @@ -1131,7 +1131,7 @@
   45.31              (map (fn (name, Def def) => (fst (mk_name prfx name), def)) ds)
   45.32    in
   45.33      seri_module (resolver []) (imports_of module [])
   45.34 -      (*map (resolver []) (Graph.strong_conn module |> List.concat |> rev)*)
   45.35 +      (*map (resolver []) (Graph.strong_conn module |> flat |> rev)*)
   45.36        (("", name_root), (mk_contents [] module))
   45.37    end;
   45.38  
    46.1 --- a/src/Pure/Tools/compute.ML	Thu Apr 27 12:11:56 2006 +0200
    46.2 +++ b/src/Pure/Tools/compute.ML	Thu Apr 27 15:06:35 2006 +0200
    46.3 @@ -24,7 +24,7 @@
    46.4  
    46.5  exception Make of string;
    46.6  
    46.7 -fun is_mono_typ (Type (_, list)) = List.all is_mono_typ list
    46.8 +fun is_mono_typ (Type (_, list)) = forall is_mono_typ list
    46.9    | is_mono_typ _ = false
   46.10  
   46.11  fun is_mono_term (Const (_, t)) = is_mono_typ t
   46.12 @@ -247,9 +247,8 @@
   46.13      let
   46.14        val (_, {mk_rews={mk=mk,mk_eq_True=emk, ...},...}) = rep_ss (simpset_of thy)
   46.15        fun mk_eq_True th = (case emk th of NONE => [th] | SOME th' => [th, th'])
   46.16 -      fun app f l = List.concat (map f l)
   46.17      in
   46.18 -      basic_make thy (app mk (app mk_eq_True ths))
   46.19 +      basic_make thy (maps mk (maps mk_eq_True ths))
   46.20      end
   46.21  
   46.22  fun compute (Computer r) naming ct =
    47.1 --- a/src/Pure/Tools/nbe_codegen.ML	Thu Apr 27 12:11:56 2006 +0200
    47.2 +++ b/src/Pure/Tools/nbe_codegen.ML	Thu Apr 27 15:06:35 2006 +0200
    47.3 @@ -131,8 +131,7 @@
    47.4          val globals = map lookup (filter defined funs);
    47.5          val default_eqn = ([params], S.app Eval_Constr (S.tup[S.quote nm,params]));
    47.6          val code = S.eqns (MLname nm)
    47.7 -                          (Library.flat(map (mk_eqn defined nm ar) eqns) 
    47.8 -                           @ [default_eqn])
    47.9 +                          (maps (mk_eqn defined nm ar) eqns @ [default_eqn])
   47.10          val register = tab_update
   47.11              (S.app Eval_mk_Fun (S.tup[S.quote nm, MLname nm, string_of_int ar]))
   47.12        in
    48.1 --- a/src/Pure/axclass.ML	Thu Apr 27 12:11:56 2006 +0200
    48.2 +++ b/src/Pure/axclass.ML	Thu Apr 27 15:06:35 2006 +0200
    48.3 @@ -267,7 +267,7 @@
    48.4  
    48.5      (* definition *)
    48.6  
    48.7 -    val conjs = map (curry Logic.mk_inclass (Term.aT [])) super @ List.concat axiomss;
    48.8 +    val conjs = map (curry Logic.mk_inclass (Term.aT [])) super @ flat axiomss;
    48.9      val class_eq =
   48.10        Logic.mk_equals (Logic.mk_inclass (Term.aT [], class), Logic.mk_conjunction_list conjs);
   48.11  
    49.1 --- a/src/Pure/codegen.ML	Thu Apr 27 12:11:56 2006 +0200
    49.2 +++ b/src/Pure/codegen.ML	Thu Apr 27 15:06:35 2006 +0200
    49.3 @@ -442,8 +442,7 @@
    49.4              | (true, "isup") => "" :: check_str zs
    49.5              | (ctrl, s') => (if ctrl then "ctrl_" ^ s' else s') :: check_str zs)
    49.6          | (ys, zs) => implode ys :: check_str zs);
    49.7 -    val s' = space_implode "_"
    49.8 -      (List.concat (map (check_str o Symbol.explode) (NameSpace.unpack s)))
    49.9 +    val s' = space_implode "_" (maps (check_str o Symbol.explode) (NameSpace.unpack s))
   49.10    in
   49.11      if Symbol.is_ascii_letter (hd (explode s')) then s' else "id_" ^ s'
   49.12    end;
   49.13 @@ -537,7 +536,7 @@
   49.14      val names = foldr add_term_names
   49.15        (map (fst o fst) (Drule.vars_of_terms ts)) ts;
   49.16      val reserved = names inter ThmDatabase.ml_reserved;
   49.17 -    val (illegal, alt_names) = split_list (List.mapPartial (fn s =>
   49.18 +    val (illegal, alt_names) = split_list (map_filter (fn s =>
   49.19        let val s' = mk_id s in if s = s' then NONE else SOME (s, s') end) names)
   49.20      val ps = (reserved @ illegal) ~~
   49.21        variantlist (map (suffix "'") reserved @ alt_names, names);
   49.22 @@ -564,7 +563,7 @@
   49.23  fun get_assoc_code thy s T = Option.map snd (Library.find_first (fn ((s', T'), _) =>
   49.24    s = s' andalso is_instance thy T T') (#consts (CodegenData.get thy)));
   49.25  
   49.26 -fun get_aux_code xs = List.mapPartial (fn (m, code) =>
   49.27 +fun get_aux_code xs = map_filter (fn (m, code) =>
   49.28    if m = "" orelse m mem !mode then SOME code else NONE) xs;
   49.29  
   49.30  fun mk_deftab thy =
   49.31 @@ -841,7 +840,7 @@
   49.32  
   49.33  fun output_code gr module xs =
   49.34    let
   49.35 -    val code = List.mapPartial (fn s =>
   49.36 +    val code = map_filter (fn s =>
   49.37        let val c as (_, module', _) = Graph.get_node gr s
   49.38        in if module = "" orelse module = module' then SOME (s, c) else NONE end)
   49.39          (rev (Graph.all_preds gr xs));
   49.40 @@ -859,9 +858,9 @@
   49.41          val modules = distinct (op =) (map (#2 o snd) code);
   49.42          val mod_gr = foldr (uncurry Graph.add_edge_acyclic)
   49.43            (foldr (uncurry (Graph.new_node o rpair ())) Graph.empty modules)
   49.44 -          (List.concat (map (fn (s, (_, module, _)) => map (pair module)
   49.45 +          (maps (fn (s, (_, module, _)) => map (pair module)
   49.46              (filter_out (equal module) (map (#2 o Graph.get_node gr)
   49.47 -              (Graph.imm_succs gr s)))) code));
   49.48 +              (Graph.imm_succs gr s)))) code);
   49.49          val modules' =
   49.50            rev (Graph.all_preds mod_gr (map (#2 o Graph.get_node gr) xs))
   49.51        in
   49.52 @@ -896,13 +895,13 @@
   49.53      val (gr', ps) = foldl_map (fn (gr, (s, t)) => apsnd (pair s)
   49.54        (invoke_codegen thy defs "<Top>" module false (gr, t)))
   49.55          (gr, map (apsnd (expand o preprocess_term thy o prep_term thy)) xs);
   49.56 -    val code = List.mapPartial
   49.57 +    val code = map_filter
   49.58        (fn ("", _) => NONE
   49.59          | (s', p) => SOME (Pretty.string_of (Pretty.block
   49.60            [Pretty.str ("val " ^ s' ^ " ="), Pretty.brk 1, p, Pretty.str ";"]))) ps;
   49.61      val code' = space_implode "\n\n" code ^ "\n\n";
   49.62      val code'' =
   49.63 -      List.mapPartial (fn (name, s) =>
   49.64 +      map_filter (fn (name, s) =>
   49.65            if "library" mem !mode andalso name = module andalso null code
   49.66            then NONE
   49.67            else SOME (name, mk_struct name s))
   49.68 @@ -923,7 +922,7 @@
   49.69  val strip_tname = implode o tl o explode;
   49.70  
   49.71  fun pretty_list xs = Pretty.block (Pretty.str "[" ::
   49.72 -  List.concat (separate [Pretty.str ",", Pretty.brk 1] (map single xs)) @
   49.73 +  flat (separate [Pretty.str ",", Pretty.brk 1] (map single xs)) @
   49.74    [Pretty.str "]"]);
   49.75  
   49.76  fun mk_type p (TVar ((s, i), _)) = Pretty.str
   49.77 @@ -940,8 +939,8 @@
   49.78        (Pretty.block (separate (Pretty.brk 1)
   49.79          (Pretty.str (mk_qual_id module
   49.80            (get_type_id' (fn s' => "term_of_" ^ s') s gr)) ::
   49.81 -        List.concat (map (fn T =>
   49.82 -          [mk_term_of gr module true T, mk_type true T]) Ts))));
   49.83 +        maps (fn T =>
   49.84 +          [mk_term_of gr module true T, mk_type true T]) Ts)));
   49.85  
   49.86  
   49.87  (**** Test data generators ****)
   49.88 @@ -985,7 +984,7 @@
   49.89                Pretty.brk 1, Pretty.str "then NONE",
   49.90                Pretty.brk 1, Pretty.str "else ",
   49.91                Pretty.block [Pretty.str "SOME ", Pretty.block (Pretty.str "[" ::
   49.92 -                List.concat (separate [Pretty.str ",", Pretty.brk 1]
   49.93 +                flat (separate [Pretty.str ",", Pretty.brk 1]
   49.94                    (map (fn ((s, T), s') => [Pretty.block
   49.95                      [Pretty.str ("(" ^ Library.quote (Symbol.escape s) ^ ","), Pretty.brk 1,
   49.96                       mk_app false (mk_term_of gr "Generated" false T)
    50.1 --- a/src/Pure/consts.ML	Thu Apr 27 12:11:56 2006 +0200
    50.2 +++ b/src/Pure/consts.ML	Thu Apr 27 15:06:35 2006 +0200
    50.3 @@ -67,7 +67,7 @@
    50.4    make_consts (f (decls, constraints, rev_abbrevs, expand_abbrevs));
    50.5  
    50.6  fun abbrevs_of (Consts ({rev_abbrevs, ...}, _)) modes =
    50.7 -  List.concat (map (Symtab.lookup_list rev_abbrevs) modes);
    50.8 +  maps (Symtab.lookup_list rev_abbrevs) modes;
    50.9  
   50.10  
   50.11  (* dest consts *)
    51.1 --- a/src/Pure/context.ML	Thu Apr 27 12:11:56 2006 +0200
    51.2 +++ b/src/Pure/context.ML	Thu Apr 27 15:06:35 2006 +0200
    51.3 @@ -380,7 +380,7 @@
    51.4      let
    51.5        val parents =
    51.6          maximal_thys (distinct eq_thy (map check_thy imports));
    51.7 -      val ancestors = distinct eq_thy (parents @ List.concat (map ancestors_of parents));
    51.8 +      val ancestors = distinct eq_thy (parents @ maps ancestors_of parents);
    51.9        val Theory ({id, ids, iids, ...}, data, _, _) =
   51.10          (case parents of
   51.11            [] => error "No parent theories"
    52.1 --- a/src/Pure/defs.ML	Thu Apr 27 12:11:56 2006 +0200
    52.2 +++ b/src/Pure/defs.ML	Thu Apr 27 15:06:35 2006 +0200
    52.3 @@ -69,7 +69,7 @@
    52.4    in (consts', specified') end);
    52.5  
    52.6  fun specifications_of (Defs {specified, ...}) c =
    52.7 -  (List.mapPartial
    52.8 +  (map_filter
    52.9      (fn (_, (false, _, _, _)) => NONE
   52.10        | (_, (true, specname, thyname, ty)) => SOME (ty, (specname, thyname))) o Inttab.dest
   52.11      o the_default Inttab.empty o Symtab.lookup specified) c;
    53.1 --- a/src/Pure/display.ML	Thu Apr 27 12:11:56 2006 +0200
    53.2 +++ b/src/Pure/display.ML	Thu Apr 27 15:06:35 2006 +0200
    53.3 @@ -188,7 +188,7 @@
    53.4            if not syn then NONE
    53.5            else SOME (prt_typ (Type (t, [])));
    53.6  
    53.7 -    val pretty_arities = List.concat o map (fn (t, ars) => map (prt_arity t) ars);
    53.8 +    val pretty_arities = maps (fn (t, ars) => map (prt_arity t) ars);
    53.9  
   53.10      fun pretty_const (c, ty) = Pretty.block
   53.11        [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
   53.12 @@ -208,8 +208,8 @@
   53.13      val tdecls = NameSpace.dest_table types;
   53.14      val arties = NameSpace.dest_table (Sign.type_space thy, arities);
   53.15      val cnsts = NameSpace.extern_table constants;
   53.16 -    val log_cnsts = List.mapPartial (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
   53.17 -    val abbrevs = List.mapPartial (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
   53.18 +    val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
   53.19 +    val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
   53.20      val cnstrs = NameSpace.extern_table constraints;
   53.21      val axms = NameSpace.extern_table axioms;
   53.22      val oras = NameSpace.extern_table oracles;
   53.23 @@ -221,8 +221,8 @@
   53.24        Pretty.big_list "classes:" (map pretty_classrel clsses),
   53.25        pretty_default default,
   53.26        pretty_witness witness,
   53.27 -      Pretty.big_list "syntactic types:" (List.mapPartial (pretty_type true) tdecls),
   53.28 -      Pretty.big_list "logical types:" (List.mapPartial (pretty_type false) tdecls),
   53.29 +      Pretty.big_list "syntactic types:" (map_filter (pretty_type true) tdecls),
   53.30 +      Pretty.big_list "logical types:" (map_filter (pretty_type false) tdecls),
   53.31        Pretty.big_list "type arities:" (pretty_arities arties),
   53.32        Pretty.big_list "logical consts:" (map pretty_const log_cnsts),
   53.33        Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs),
    54.1 --- a/src/Pure/drule.ML	Thu Apr 27 12:11:56 2006 +0200
    54.2 +++ b/src/Pure/drule.ML	Thu Apr 27 15:06:35 2006 +0200
    54.3 @@ -534,7 +534,7 @@
    54.4  fun thas RLN (i,thbs) =
    54.5    let val resolve = biresolution false (map (pair false) thas) i
    54.6        fun resb thb = Seq.list_of (resolve thb) handle THM _ => []
    54.7 -  in  List.concat (map resb thbs)  end;
    54.8 +  in maps resb thbs end;
    54.9  
   54.10  fun thas RL thbs = thas RLN (1,thbs);
   54.11  
   54.12 @@ -961,8 +961,8 @@
   54.13    let
   54.14      fun err msg =
   54.15        raise TYPE ("instantiate': " ^ msg,
   54.16 -        List.mapPartial (Option.map Thm.typ_of) cTs,
   54.17 -        List.mapPartial (Option.map Thm.term_of) cts);
   54.18 +        map_filter (Option.map Thm.typ_of) cTs,
   54.19 +        map_filter (Option.map Thm.term_of) cts);
   54.20  
   54.21      fun inst_of (v, ct) =
   54.22        (Thm.cterm_of (Thm.theory_of_cterm ct) (Var v), ct)
    55.1 --- a/src/Pure/goal.ML	Thu Apr 27 12:11:56 2006 +0200
    55.2 +++ b/src/Pure/goal.ML	Thu Apr 27 15:06:35 2006 +0200
    55.3 @@ -123,7 +123,7 @@
    55.4      val frees = Term.add_frees statement [];
    55.5      val fixed_frees = filter_out (member (op =) xs o #1) frees;
    55.6      val fixed_tfrees = fold (Term.add_tfreesT o #2) fixed_frees [];
    55.7 -    val params = List.mapPartial (fn x => Option.map (pair x) (AList.lookup (op =) frees x)) xs;
    55.8 +    val params = map_filter (fn x => Option.map (pair x) (AList.lookup (op =) frees x)) xs;
    55.9  
   55.10      fun err msg = cat_error msg
   55.11        ("The error(s) above occurred for the goal statement:\n" ^
    56.1 --- a/src/Pure/meta_simplifier.ML	Thu Apr 27 12:11:56 2006 +0200
    56.2 +++ b/src/Pure/meta_simplifier.ML	Thu Apr 27 15:06:35 2006 +0200
    56.3 @@ -398,7 +398,7 @@
    56.4  fun rewrite_rule_extra_vars prems elhs erhs =
    56.5    not (term_varnames erhs subset fold add_term_varnames prems (term_varnames elhs))
    56.6    orelse
    56.7 -  not (term_tvars erhs subset (term_tvars elhs union List.concat (map term_tvars prems)));
    56.8 +  not (term_tvars erhs subset (term_tvars elhs union maps term_tvars prems));
    56.9  
   56.10  (*simple test for looping rewrite rules and stupid orientations*)
   56.11  fun default_reorient thy prems lhs rhs =
   56.12 @@ -488,16 +488,16 @@
   56.13    end;
   56.14  
   56.15  fun extract_rews (Simpset (_, {mk_rews = {mk, ...}, ...}), thms) =
   56.16 -  List.concat (map (fn thm => map (rpair (Thm.name_of_thm thm)) (mk thm)) thms);
   56.17 +  maps (fn thm => map (rpair (Thm.name_of_thm thm)) (mk thm)) thms;
   56.18  
   56.19  fun orient_comb_simps comb mk_rrule (ss, thms) =
   56.20    let
   56.21      val rews = extract_rews (ss, thms);
   56.22 -    val rrules = List.concat (map mk_rrule rews);
   56.23 +    val rrules = maps mk_rrule rews;
   56.24    in Library.foldl comb (ss, rrules) end;
   56.25  
   56.26  fun extract_safe_rrules (ss, thm) =
   56.27 -  List.concat (map (orient_rrule ss) (extract_rews (ss, [thm])));
   56.28 +  maps (orient_rrule ss) (extract_rews (ss, [thm]));
   56.29  
   56.30  (*add rewrite rules explicitly; do not reorient!*)
   56.31  fun ss addsimps thms =
   56.32 @@ -570,7 +570,7 @@
   56.33          raise SIMPLIFIER ("Congruence must start with a constant", thm);
   56.34        val (alist, _) = congs;
   56.35        val alist2 = List.filter (fn (x, _) => x <> a) alist;
   56.36 -      val weak2 = alist2 |> List.mapPartial (fn (a, {thm, ...}: cong) =>
   56.37 +      val weak2 = alist2 |> map_filter (fn (a, {thm, ...}: cong) =>
   56.38          if is_full_cong thm then NONE else SOME a);
   56.39      in ((alist2, weak2), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);
   56.40  
   56.41 @@ -1037,7 +1037,7 @@
   56.42          in (extract_safe_rrules (ss, asm), SOME asm) end
   56.43  
   56.44      and add_rrules (rrss, asms) ss =
   56.45 -      Library.foldl (insert_rrule true) (ss, List.concat rrss) |> add_prems (List.mapPartial I asms)
   56.46 +      Library.foldl (insert_rrule true) (ss, flat rrss) |> add_prems (map_filter I asms)
   56.47  
   56.48      and disch r (prem, eq) =
   56.49        let
    57.1 --- a/src/Pure/net.ML	Thu Apr 27 12:11:56 2006 +0200
    57.2 +++ b/src/Pure/net.ML	Thu Apr 27 15:06:35 2006 +0200
    57.3 @@ -197,7 +197,7 @@
    57.4                 | _ => rands t (net, var::nets)  (*var could match also*)
    57.5    end;
    57.6  
    57.7 -fun extract_leaves l = List.concat (map (fn Leaf(xs) => xs) l);
    57.8 +fun extract_leaves l = maps (fn Leaf xs => xs) l;
    57.9  
   57.10  (*return items whose key could match t, WHICH MUST BE BETA-ETA NORMAL*)
   57.11  fun match_term net t =
   57.12 @@ -236,7 +236,7 @@
   57.13    | dest (Net {comb, var, atoms}) =
   57.14        map (cons_fst CombK) (dest comb) @
   57.15        map (cons_fst VarK) (dest var) @
   57.16 -      List.concat (map (fn (a, net) => map (cons_fst (AtomK a)) (dest net)) (Symtab.dest atoms));
   57.17 +      maps (fn (a, net) => map (cons_fst (AtomK a)) (dest net)) (Symtab.dest atoms);
   57.18  
   57.19  fun merge eq (net1, net2) = fold (insert_safe eq) (dest net2) net1;
   57.20  
    58.1 --- a/src/Pure/pattern.ML	Thu Apr 27 12:11:56 2006 +0200
    58.2 +++ b/src/Pure/pattern.ML	Thu Apr 27 15:06:35 2006 +0200
    58.3 @@ -177,7 +177,7 @@
    58.4                        let val js = ints_of' env ts;
    58.5                            val js' = map (try (trans d)) js;
    58.6                            val ks = mk_proj_list js';
    58.7 -                          val ls = List.mapPartial I js'
    58.8 +                          val ls = map_filter I js'
    58.9                            val Hty = type_of_G env (Fty,length js,ks)
   58.10                            val (env',H) = Envir.genvar a (env,Hty)
   58.11                            val env'' =
    59.1 --- a/src/Pure/proof_general.ML	Thu Apr 27 12:11:56 2006 +0200
    59.2 +++ b/src/Pure/proof_general.ML	Thu Apr 27 15:06:35 2006 +0200
    59.3 @@ -493,7 +493,7 @@
    59.4  in
    59.5  
    59.6  fun setup_present_hook () =
    59.7 -  Present.add_hook (fn _ => fn res => tell_thm_deps (List.concat (map #2 res)));
    59.8 +  Present.add_hook (fn _ => fn res => tell_thm_deps (maps #2 res));
    59.9  
   59.10  end;
   59.11  
   59.12 @@ -1456,7 +1456,7 @@
   59.13    "\n  '(" ^ space_implode "\n    " (map (quote o regexp_quote) strs) ^ "))\n";
   59.14  
   59.15  fun make_elisp_commands commands kind = defconst kind
   59.16 -  (commands |> List.mapPartial (fn (c, _, k, _) => if k = kind then SOME c else NONE));
   59.17 +  (commands |> map_filter (fn (c, _, k, _) => if k = kind then SOME c else NONE));
   59.18  
   59.19  fun make_elisp_syntax (keywords, commands) =
   59.20    ";;\n\
    60.1 --- a/src/Pure/proofterm.ML	Thu Apr 27 12:11:56 2006 +0200
    60.2 +++ b/src/Pure/proofterm.ML	Thu Apr 27 15:06:35 2006 +0200
    60.3 @@ -414,15 +414,15 @@
    60.4  (**** substitutions ****)
    60.5  
    60.6  fun del_conflicting_tvars envT T = Term.instantiateT
    60.7 -  (List.mapPartial (fn ixnS as (_, S) =>
    60.8 +  (map_filter (fn ixnS as (_, S) =>
    60.9       (Type.lookup (envT, ixnS); NONE) handle TYPE _ =>
   60.10          SOME (ixnS, TFree ("'dummy", S))) (typ_tvars T)) T;
   60.11  
   60.12  fun del_conflicting_vars env t = Term.instantiate
   60.13 -  (List.mapPartial (fn ixnS as (_, S) =>
   60.14 +  (map_filter (fn ixnS as (_, S) =>
   60.15       (Type.lookup (type_env env, ixnS); NONE) handle TYPE _ =>
   60.16          SOME (ixnS, TFree ("'dummy", S))) (term_tvars t),
   60.17 -   List.mapPartial (fn Var (ixnT as (_, T)) =>
   60.18 +   map_filter (fn Var (ixnT as (_, T)) =>
   60.19       (Envir.lookup (env, ixnT); NONE) handle TYPE _ =>
   60.20          SOME (ixnT, Free ("dummy", T))) (term_vars t)) t;
   60.21  
   60.22 @@ -836,7 +836,7 @@
   60.23  
   60.24  fun add_funvars Ts (vs, t) =
   60.25    if is_fun (fastype_of1 (Ts, t)) then
   60.26 -    vs union List.mapPartial (fn Var (ixn, T) =>
   60.27 +    vs union map_filter (fn Var (ixn, T) =>
   60.28        if is_fun T then SOME ixn else NONE | _ => NONE) (vars_of t)
   60.29    else vs;
   60.30  
   60.31 @@ -903,7 +903,7 @@
   60.32            in (b, is, ch, if ch then Abst (a, Option.map compress_typ T, body') else prf) end
   60.33        | shrink ls lev (prf as AbsP (a, t, body)) =
   60.34            let val (b, is, ch, body') = shrink (lev::ls) lev body
   60.35 -          in (b orelse member (op =) is 0, List.mapPartial (fn 0 => NONE | i => SOME (i-1)) is,
   60.36 +          in (b orelse member (op =) is 0, map_filter (fn 0 => NONE | i => SOME (i-1)) is,
   60.37              ch, if ch then AbsP (a, Option.map compress_term t, body') else prf)
   60.38            end
   60.39        | shrink ls lev prf =
    61.1 --- a/src/Pure/pure_thy.ML	Thu Apr 27 12:11:56 2006 +0200
    61.2 +++ b/src/Pure/pure_thy.ML	Thu Apr 27 15:06:35 2006 +0200
    61.3 @@ -219,7 +219,7 @@
    61.4              error ("Bad subscript " ^ string_of_int i ^ " for " ^
    61.5                quote name ^ " (length " ^ string_of_int n ^ ")")
    61.6            else List.nth (thms, i - 1);
    61.7 -      in map select (List.concat (map (interval n) is)) end;
    61.8 +      in map select (maps (interval n) is) end;
    61.9  
   61.10  
   61.11  (* selections *)
   61.12 @@ -263,7 +263,7 @@
   61.13      |> the_thms name |> select_thm thmref |> map (Thm.transfer theory)
   61.14    end;
   61.15  
   61.16 -fun get_thmss thy thmrefs = List.concat (map (get_thms thy) thmrefs);
   61.17 +fun get_thmss thy thmrefs = maps (get_thms thy) thmrefs;
   61.18  fun get_thm thy thmref = single_thm (name_of_thmref thmref) (get_thms thy thmref);
   61.19  
   61.20  fun thm name = get_thm (the_context ()) (Name name);
   61.21 @@ -279,14 +279,13 @@
   61.22  
   61.23  fun thms_containing theory spec =
   61.24    (theory :: Theory.ancestors_of theory)
   61.25 -  |> map (fn thy =>
   61.26 +  |> maps (fn thy =>
   61.27        FactIndex.find (fact_index_of thy) spec
   61.28        |> List.filter (fn (name, ths) => valid_thms theory (Name name, ths))
   61.29 -      |> distinct (eq_fst (op =)))
   61.30 -  |> List.concat;
   61.31 +      |> distinct (eq_fst (op =)));
   61.32  
   61.33  fun thms_containing_consts thy consts =
   61.34 -  thms_containing thy (consts, []) |> map #2 |> List.concat
   61.35 +  thms_containing thy (consts, []) |> maps #2
   61.36    |> map (fn th => (Thm.name_of_thm th, th));
   61.37  
   61.38  
   61.39 @@ -294,9 +293,9 @@
   61.40  
   61.41  fun thms_of thy =
   61.42    let val thms = #2 (theorems_of thy)
   61.43 -  in map (fn th => (Thm.name_of_thm th, th)) (List.concat (map snd (Symtab.dest thms))) end;
   61.44 +  in map (fn th => (Thm.name_of_thm th, th)) (maps snd (Symtab.dest thms)) end;
   61.45  
   61.46 -fun all_thms_of thy = List.concat (map thms_of (thy :: Theory.ancestors_of thy));
   61.47 +fun all_thms_of thy = maps thms_of (thy :: Theory.ancestors_of thy);
   61.48  
   61.49  
   61.50  
   61.51 @@ -379,7 +378,7 @@
   61.52    let
   61.53      fun app (x, (ths, atts)) = foldl_map (Thm.theory_attributes atts) (x, ths);
   61.54      val (thms, thy') = thy |> enter_thms
   61.55 -      name_thmss (name_thms false) (apsnd List.concat o foldl_map app)
   61.56 +      name_thmss (name_thms false) (apsnd flat o foldl_map app)
   61.57        (bname, map (fn (ths, atts) => (get thy ths, atts @ more_atts @ [kind k])) ths_atts);
   61.58    in ((bname, thms), thy') end);
   61.59  
    62.1 --- a/src/Pure/search.ML	Thu Apr 27 12:11:56 2006 +0200
    62.2 +++ b/src/Pure/search.ML	Thu Apr 27 15:06:35 2006 +0200
    62.3 @@ -243,7 +243,7 @@
    62.4  	      ([],[]) => []
    62.5  	    | ([],nonsats) => 
    62.6  		  (message("breadth=" ^ string_of_int(length nonsats));
    62.7 -		   bfs (List.concat (map tacf nonsats)))
    62.8 +		   bfs (maps tacf nonsats))
    62.9  	    | (sats,_)  => sats)
   62.10    in (fn st => Seq.of_list (bfs [st])) end;
   62.11  
    63.1 --- a/src/Pure/sign.ML	Thu Apr 27 12:11:56 2006 +0200
    63.2 +++ b/src/Pure/sign.ML	Thu Apr 27 15:06:35 2006 +0200
    63.3 @@ -345,7 +345,7 @@
    63.4  fun mapping add_names f t =
    63.5    let
    63.6      fun f' x = let val y = f x in if x = y then NONE else SOME (x, y) end;
    63.7 -    val tab = List.mapPartial f' (add_names t []);
    63.8 +    val tab = map_filter f' (add_names t []);
    63.9      fun get x = the_default x (AList.lookup (op =) tab x);
   63.10    in get end;
   63.11  
   63.12 @@ -385,7 +385,7 @@
   63.13  fun pretty_typ thy T = Syntax.pretty_typ (Context.Theory thy) (syn_of thy) (extern_typ thy T);
   63.14  fun pretty_sort thy S = Syntax.pretty_sort (Context.Theory thy) (syn_of thy) (extern_sort thy S);
   63.15  
   63.16 -fun pretty_classrel thy cs = Pretty.block (List.concat
   63.17 +fun pretty_classrel thy cs = Pretty.block (flat
   63.18    (separate [Pretty.str " <", Pretty.brk 1] (map (single o pretty_sort thy o single) cs)));
   63.19  
   63.20  fun pretty_arity thy (a, Ss, S) =
   63.21 @@ -597,8 +597,8 @@
   63.22        handle TYPE (msg, _, _) => Exn (ERROR msg);
   63.23  
   63.24      val err_results = map infer termss;
   63.25 -    val errs = List.mapPartial (fn Exn (ERROR msg) => SOME msg | _ => NONE) err_results;
   63.26 -    val results = List.mapPartial get_result err_results;
   63.27 +    val errs = map_filter (fn Exn (ERROR msg) => SOME msg | _ => NONE) err_results;
   63.28 +    val results = map_filter get_result err_results;
   63.29  
   63.30      val ambiguity = length termss;
   63.31      fun ambig_msg () =
   63.32 @@ -614,7 +614,7 @@
   63.33            \You may still want to disambiguate your grammar or your input."
   63.34        else (); hd results)
   63.35      else (cat_error (ambig_msg ()) ("More than one term is type correct:\n" ^
   63.36 -      cat_lines (map (Pretty.string_of_term pp) (List.concat (map fst results)))))
   63.37 +      cat_lines (map (Pretty.string_of_term pp) (maps fst results))))
   63.38    end;
   63.39  
   63.40  fun infer_types pp thy consts def_type def_sort used freeze tsT =
    64.1 --- a/src/Pure/sorts.ML	Thu Apr 27 12:11:56 2006 +0200
    64.2 +++ b/src/Pure/sorts.ML	Thu Apr 27 15:06:35 2006 +0200
    64.3 @@ -248,7 +248,7 @@
    64.4        | check_result (SOME (T, S)) =
    64.5            if of_sort (classes, arities) (T, S) then SOME (T, S)
    64.6            else sys_error ("Sorts.witness_sorts: bad witness for sort " ^ str_of_sort S);
    64.7 -  in List.mapPartial check_result (#2 (witness_aux (classes, arities) log_types hyps sorts)) end;
    64.8 +  in map_filter check_result (#2 (witness_aux (classes, arities) log_types hyps sorts)) end;
    64.9  
   64.10  end;
   64.11  
    65.1 --- a/src/Pure/tactic.ML	Thu Apr 27 12:11:56 2006 +0200
    65.2 +++ b/src/Pure/tactic.ML	Thu Apr 27 15:06:35 2006 +0200
    65.3 @@ -462,8 +462,7 @@
    65.4      (fn (prem,i) =>
    65.5        let val hyps = Logic.strip_assums_hyp prem
    65.6            and concl = Logic.strip_assums_concl prem
    65.7 -          val kbrls = Net.unify_term inet concl @
    65.8 -                      List.concat (map (Net.unify_term enet) hyps)
    65.9 +          val kbrls = Net.unify_term inet concl @ maps (Net.unify_term enet) hyps
   65.10        in PRIMSEQ (biresolution match (order kbrls) i) end);
   65.11  
   65.12  (*versions taking pre-built nets.  No filtering of brls*)
    66.1 --- a/src/Pure/theory.ML	Thu Apr 27 12:11:56 2006 +0200
    66.2 +++ b/src/Pure/theory.ML	Thu Apr 27 15:06:35 2006 +0200
    66.3 @@ -144,7 +144,7 @@
    66.4  val oracle_space = #1 o #oracles o rep_theory;
    66.5  
    66.6  val axioms_of = Symtab.dest o #2 o #axioms o rep_theory;
    66.7 -fun all_axioms_of thy = List.concat (map axioms_of (thy :: ancestors_of thy));
    66.8 +fun all_axioms_of thy = maps axioms_of (thy :: ancestors_of thy);
    66.9  
   66.10  val defs_of = #defs o rep_theory;
   66.11  
    67.1 --- a/src/Pure/type_infer.ML	Thu Apr 27 12:11:56 2006 +0200
    67.2 +++ b/src/Pure/type_infer.ML	Thu Apr 27 15:06:35 2006 +0200
    67.3 @@ -413,7 +413,7 @@
    67.4      (*collect result unifier*)
    67.5      fun ch_var (xi, Link (r as ref (Param S))) = (r := PTVar (xi, S); NONE)
    67.6        | ch_var xi_T = SOME xi_T;
    67.7 -    val env = List.mapPartial ch_var Tps;
    67.8 +    val env = map_filter ch_var Tps;
    67.9  
   67.10      (*convert back to terms/typs*)
   67.11      val mk_var =