# HG changeset patch # User wenzelm # Date 1146143195 -7200 # Node ID 9f11af8f7ef910f51495439f3275f93a80faeb07 # Parent a6205c6203ea3445841afa1e9fca0df829d5da3c tuned basic list operators (flat, maps, map_filter); diff -r a6205c6203ea -r 9f11af8f7ef9 src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Provers/Arith/fast_lin_arith.ML Thu Apr 27 15:06:35 2006 +0200 @@ -327,7 +327,7 @@ (* ------------------------------------------------------------------------- *) fun allpairs f xs ys = - List.concat(map (fn x => map (fn y => f x y) ys) xs); + maps (fn x => map (fn y => f x y) ys) xs; fun extract_first p = let fun extract xs (y::ys) = if p y then (SOME y,xs@ys) @@ -414,7 +414,7 @@ val simpset' = Simplifier.inherit_context ss simpset; val atoms = Library.foldl (fn (ats,(lhs,_,_,rhs,_,_)) => map fst lhs union (map fst rhs union ats)) - ([], List.mapPartial (fn thm => if Thm.no_prems thm + ([], map_filter (fn thm => if Thm.no_prems thm then LA_Data.decomp sg (concl_of thm) else NONE) asms) @@ -596,7 +596,7 @@ val mkleq = mklineq n atoms val ixs = 0 upto (n-1) val iatoms = atoms ~~ ixs - val natlineqs = List.mapPartial (mknat pTs ixs) iatoms + val natlineqs = map_filter (mknat pTs ixs) iatoms val ineqs = map mkleq initems @ natlineqs in case elim(ineqs,[]) of Success(j) => @@ -726,7 +726,7 @@ *) fun lin_arith_prover sg ss concl = let - val thms = List.concat(map LA_Logic.atomize (prems_of_ss ss)); + val thms = maps LA_Logic.atomize (prems_of_ss ss); val Hs = map (#prop o rep_thm) thms val Tconcl = LA_Logic.mk_Trueprop concl in case prove sg ([],[]) false Hs Tconcl of (* concl provable? *) diff -r a6205c6203ea -r 9f11af8f7ef9 src/Provers/blast.ML --- a/src/Provers/blast.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Provers/blast.ML Thu Apr 27 15:06:35 2006 +0200 @@ -538,16 +538,12 @@ case P of (Const ("*Goal*", _) $ G) => let val pG = mk_Trueprop (toTerm 2 G) - val intrs = List.concat - (map (fn (inet,_) => Net.unify_term inet pG) - nps) + val intrs = maps (fn (inet,_) => Net.unify_term inet pG) nps in map (fromIntrRule vars o #2) (Tactic.orderlist intrs) end | _ => let val pP = mk_Trueprop (toTerm 3 P) - val elims = List.concat - (map (fn (_,enet) => Net.unify_term enet pP) - nps) - in List.mapPartial (fromRule vars o #2) (Tactic.orderlist elims) end; + val elims = maps (fn (_,enet) => Net.unify_term enet pP) nps + in map_filter (fromRule vars o #2) (Tactic.orderlist elims) end; (*Pending formulae carry md (may duplicate) flags*) diff -r a6205c6203ea -r 9f11af8f7ef9 src/Provers/induct_method.ML --- a/src/Provers/induct_method.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Provers/induct_method.ML Thu Apr 27 15:06:35 2006 +0200 @@ -80,7 +80,7 @@ val xs = InductAttrib.vars_of tm; in align "Rule has fewer variables than instantiations given" xs ts - |> List.mapPartial prep_var + |> map_filter prep_var end; @@ -129,7 +129,7 @@ fun inst_rule r = if null insts then `RuleCases.get r else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts - |> (List.concat o map (prep_inst thy align_left I)) + |> maps (prep_inst thy align_left I) |> Drule.cterm_instantiate) r |> pair (RuleCases.get r); val ruleq = @@ -333,7 +333,7 @@ in ((SOME (Free lhs), [def]), ctxt') end | add (SOME (NONE, t)) ctxt = ((SOME t, []), ctxt) | add NONE ctxt = ((NONE, []), ctxt); - in fold_map add def_insts #> apfst (split_list #> apsnd List.concat) end; + in fold_map add def_insts #> apfst (split_list #> apsnd flat) end; (* induct_tac *) @@ -348,7 +348,7 @@ local fun find_inductT ctxt insts = - fold_rev multiply (insts |> List.mapPartial (fn [] => NONE | ts => List.last ts) + fold_rev multiply (insts |> map_filter (fn [] => NONE | ts => List.last ts) |> map (InductAttrib.find_inductT ctxt o Term.fastype_of)) [[]] |> filter_out (forall PureThy.is_internal); @@ -370,7 +370,7 @@ (if null insts then `RuleCases.get r else (align_left "Rule has fewer conclusions than arguments given" (map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts - |> (List.concat o map (prep_inst thy align_right (atomize_term thy))) + |> maps (prep_inst thy align_right (atomize_term thy)) |> Drule.cterm_instantiate) r |> pair (RuleCases.get r)) |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th)); @@ -380,7 +380,7 @@ | NONE => (find_inductS ctxt facts @ map (special_rename_params defs_ctxt insts) (find_inductT ctxt insts)) - |> List.mapPartial RuleCases.mutual_rule + |> map_filter RuleCases.mutual_rule |> tap (trace_rules ctxt InductAttrib.inductN o map #2) |> Seq.of_list |> Seq.maps (Seq.try inst_rule)); @@ -389,7 +389,7 @@ in (fn i => fn st => ruleq - |> Seq.maps (RuleCases.consume (List.concat defs) facts) + |> Seq.maps (RuleCases.consume (flat defs) facts) |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) => (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j => (CONJUNCTS (ALLGOALS diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/General/graph.ML --- a/src/Pure/General/graph.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/General/graph.ML Thu Apr 27 15:06:35 2006 +0200 @@ -132,13 +132,13 @@ fun imm_succs G = #2 o #2 o get_entry G; (*transitive*) -fun all_preds G = List.concat o fst o reachable (imm_preds G); -fun all_succs G = List.concat o fst o reachable (imm_succs G); +fun all_preds G = flat o fst o reachable (imm_preds G); +fun all_succs G = flat o fst o reachable (imm_succs G); (*strongly connected components; see: David King and John Launchbury, "Structuring Depth First Search Algorithms in Haskell"*) fun strong_conn G = filter_out null (fst (reachable (imm_preds G) - (List.concat (rev (fst (reachable (imm_succs G) (keys G))))))); + (flat (rev (fst (reachable (imm_succs G) (keys G))))))); (*subgraph induced by node subset*) fun subgraph keys (Graph tab) = @@ -157,7 +157,7 @@ fun paths ps p = if not (null ps) andalso eq_key (p, x) then [p :: ps] else if member_keys X p andalso not (member_key ps p) - then List.concat (map (paths (p :: ps)) (imm_preds G p)) + then maps (paths (p :: ps)) (imm_preds G p) else []; in paths [] y end; @@ -194,7 +194,7 @@ else G; fun diff_edges G1 G2 = - List.concat (dest G1 |> map (fn (x, ys) => ys |> List.mapPartial (fn y => + flat (dest G1 |> map (fn (x, ys) => ys |> map_filter (fn y => if is_edge G2 (x, y) then NONE else SOME (x, y)))); fun edges G = diff_edges G empty; diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/General/path.ML --- a/src/Pure/General/path.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/General/path.ML Thu Apr 27 15:06:35 2006 +0200 @@ -153,7 +153,7 @@ | path => rep (unpack path)) | eval x = [x]; -val expand = rep #> map eval #> List.concat #> norm #> Path; +val expand = rep #> maps eval #> norm #> Path; val position = expand #> pack #> quote #> Position.line_name 1; end; diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/General/pretty.ML --- a/src/Pure/General/pretty.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/General/pretty.ML Thu Apr 27 15:06:35 2006 +0200 @@ -219,13 +219,13 @@ val strs = block o breaks o map str; fun chunks prts = blk (0, fbreaks prts); -fun chunks2 prts = blk (0, List.concat (Library.separate [fbrk, fbrk] (map single prts))); +fun chunks2 prts = blk (0, flat (Library.separate [fbrk, fbrk] (map single prts))); fun quote prt = blk (1, [str "\"", prt, str "\""]); fun backquote prt = blk (1, [str "`", prt, str "`"]); fun separate sep prts = - List.concat (Library.separate [str sep, brk 1] (map single prts)); + flat (Library.separate [str sep, brk 1] (map single prts)); val commas = separate ","; diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/General/table.ML --- a/src/Pure/General/table.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/General/table.ML Thu Apr 27 15:06:35 2006 +0200 @@ -379,7 +379,7 @@ handle UNDEF _ => delete key tab; fun make_list args = fold_rev update_list args empty; -fun dest_list tab = List.concat (map (fn (key, xs) => map (pair key) xs) (dest tab)); +fun dest_list tab = maps (fn (key, xs) => map (pair key) xs) (dest tab); fun merge_list eq = join (fn _ => Library.merge eq); diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/General/xml.ML --- a/src/Pure/General/xml.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/General/xml.ML Thu Apr 27 15:06:35 2006 +0200 @@ -134,7 +134,7 @@ || parse_pi >> K [] || parse_comment >> K []) -- Scan.optional ((* scan_whspc |-- *) parse_chars >> (single o Text)) [] - >> op @) >> List.concat) >> op @)(* --| scan_whspc*)) xs + >> op @) >> flat) >> op @)(* --| scan_whspc*)) xs and parse_elem xs = ($$ "<" |-- Symbol.scan_id -- diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/IsaPlanner/isand.ML --- a/src/Pure/IsaPlanner/isand.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/IsaPlanner/isand.ML Thu Apr 27 15:06:35 2006 +0200 @@ -257,7 +257,7 @@ val prop = (Thm.prop_of th); val tvars = List.foldr Term.add_term_tvars [] (prop :: tpairs); val ctyfixes = - Library.mapfilter + map_filter (fn (v as ((s,i),ty)) => if i <= ix then SOME (ctypify (TVar v), ctypify (TFree (s,ty))) else NONE) tvars; @@ -271,7 +271,7 @@ val vars = map Term.dest_Var (List.foldr Term.add_term_vars [] (prop :: tpairs)); val cfixes = - Library.mapfilter + map_filter (fn (v as ((s,i),ty)) => if i <= ix then SOME (ctermify (Var v), ctermify (Free (s,ty))) else NONE) vars; diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/IsaPlanner/term_lib.ML --- a/src/Pure/IsaPlanner/term_lib.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/IsaPlanner/term_lib.ML Thu Apr 27 15:06:35 2006 +0200 @@ -428,8 +428,7 @@ | term_contains1 T (ah $ at) (bh $ bt) = (term_contains1 T ah (bh $ bt)) @ (term_contains1 T at (bh $ bt)) @ - (List.concat (map (fn inT => (term_contains1 inT at bt)) - (term_contains1 T ah bh))) + (maps (fn inT => (term_contains1 inT at bt)) (term_contains1 T ah bh)) | term_contains1 T a (bh $ bt) = [] diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Isar/args.ML --- a/src/Pure/Isar/args.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/Isar/args.ML Thu Apr 27 15:06:35 2006 +0200 @@ -352,7 +352,7 @@ ((Scan.repeat1 (Scan.repeat1 (atomic blk) || argsp "(" ")" || - argsp "[" "]")) >> List.concat) x + argsp "[" "]")) >> flat) x and argsp l r x = (Scan.trace (&&& l -- !!! (args true -- &&& r)) >> #2) x; diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/Isar/attrib.ML Thu Apr 27 15:06:35 2006 +0200 @@ -164,7 +164,7 @@ val thm = gen_thm PureThy.single_thm; val multi_thm = gen_thm (K I); -val thms = Scan.repeat multi_thm >> List.concat; +val thms = Scan.repeat multi_thm >> flat; end; @@ -250,11 +250,11 @@ val ctxt = Context.proof_of generic; val (type_insts, term_insts) = List.partition (is_tvar o fst) (map snd mixed_insts); - val internal_insts = term_insts |> List.mapPartial + val internal_insts = term_insts |> map_filter (fn (xi, Args.Term t) => SOME (xi, t) | (_, Args.Name _) => NONE | (xi, _) => error_var "Term argument expected for " xi); - val external_insts = term_insts |> List.mapPartial + val external_insts = term_insts |> map_filter (fn (xi, Args.Name s) => SOME (xi, s) | _ => NONE); diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Isar/context_rules.ML --- a/src/Pure/Isar/context_rules.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/Isar/context_rules.ML Thu Apr 27 15:06:35 2006 +0200 @@ -118,7 +118,7 @@ val ctxt = Context.proof_of generic; fun prt_kind (i, b) = Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":") - (List.mapPartial (fn (_, (k, th)) => + (map_filter (fn (_, (k, th)) => if k = (i, b) then SOME (ProofContext.pretty_thm ctxt th) else NONE) (sort (int_ord o pairself fst) rules)); in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end; diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/Isar/element.ML Thu Apr 27 15:06:35 2006 +0200 @@ -100,7 +100,7 @@ |> Option.map (fn v => (certT (TVar v), certT T)); in Drule.tvars_intr_list (map fst subst) #-> - (fn vs => Thm.instantiate (List.mapPartial (inst vs) subst, [])) + (fn vs => Thm.instantiate (map_filter (inst vs) subst, [])) end; fun instantiate_frees thy subst = @@ -144,7 +144,7 @@ fun rename_thm ren th = let val subst = Drule.frees_of th - |> List.mapPartial (fn (x, T) => + |> map_filter (fn (x, T) => let val x' = rename ren x in if x = x' then NONE else SOME ((x, T), (Free (x', T))) end); in @@ -169,7 +169,7 @@ fun instT_subst env th = Drule.tfrees_of th - |> List.mapPartial (fn (a, S) => + |> map_filter (fn (a, S) => let val T = TFree (a, S); val T' = the_default T (Symtab.lookup env a); @@ -209,7 +209,7 @@ let val substT = instT_subst envT th; val subst = Drule.frees_of th - |> List.mapPartial (fn (x, T) => + |> map_filter (fn (x, T) => let val T' = instT_type envT T; val t = Free (x, T'); @@ -291,7 +291,7 @@ | prt_fact (ths, atts) = Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths)) :: Args.pretty_attribs ctxt atts; fun prt_note (a, ths) = - Pretty.block (Pretty.breaks (List.concat (prt_name_atts a "=" :: map prt_fact ths))); + Pretty.block (Pretty.breaks (flat (prt_name_atts a "=" :: map prt_fact ths))); in fn Fixes fixes => pretty_items "fixes" "and" (map prt_fix fixes) | Constrains xs => pretty_items "constrains" "and" (map prt_constrain xs) diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Isar/find_theorems.ML --- a/src/Pure/Isar/find_theorems.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/Isar/find_theorems.ML Thu Apr 27 15:06:35 2006 +0200 @@ -93,7 +93,7 @@ val match_thm = matches o refine_term; in map (substsize o refine_term) - (List.filter match_thm (extract_terms term_src)) |> bestmatch + (filter match_thm (extract_terms term_src)) |> bestmatch end; @@ -124,7 +124,7 @@ val prems = Logic.prems_of_goal goal 1; fun try_subst prem = is_matching_thm extract_dest ctxt true prem thm; - val successful = prems |> List.mapPartial try_subst; + val successful = prems |> map_filter try_subst; in (*if possible, keep best substitution (one with smallest size)*) (*dest rules always have assumptions, so a dest with one @@ -155,7 +155,7 @@ fun goal_tree prem = (combine prem goal_concl); fun try_subst prem = is_matching_thm (single, I) ctxt true (goal_tree prem) rule_tree; - val successful = prems |> List.mapPartial try_subst; + val successful = prems |> map_filter try_subst; in (*elim rules always have assumptions, so an elim with one assumption is as good as an intro rule with none*) @@ -226,7 +226,7 @@ prod_ord int_ord int_ord ((p1, s1), (p0, s0)); in map (`(eval_filters filters)) thms - |> List.mapPartial (fn (SOME x, y) => SOME (x, y) | (NONE, _) => NONE) + |> map_filter (fn (SOME x, y) => SOME (x, y) | (NONE, _) => NONE) |> sort thm_ord |> map #2 end; @@ -237,11 +237,9 @@ fun find_thms ctxt spec = (PureThy.thms_containing (ProofContext.theory_of ctxt) spec - |> map PureThy.selections - |> List.concat) @ + |> maps PureThy.selections) @ (ProofContext.lthms_containing ctxt spec - |> map PureThy.selections - |> List.concat + |> maps PureThy.selections |> distinct (fn ((r1, th1), (r2, th2)) => r1 = r2 andalso Drule.eq_thm_prop (th1, th2))); diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/Isar/isar_syn.ML Thu Apr 27 15:06:35 2006 +0200 @@ -239,7 +239,7 @@ val declareP = OuterSyntax.command "declare" "declare theorems (improper)" K.thy_script - (P.opt_locale_target -- (P.and_list1 P.xthms1 >> List.concat) + (P.opt_locale_target -- (P.and_list1 P.xthms1 >> flat) >> (Toplevel.theory_context o uncurry IsarThy.declare_theorems)); diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Isar/isar_thy.ML --- a/src/Pure/Isar/isar_thy.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/Isar/isar_thy.ML Thu Apr 27 15:06:35 2006 +0200 @@ -80,8 +80,8 @@ PureThy.note_thmss_i kind args #> tap (present_theorems kind); -fun apply_theorems args = apfst (List.concat o map snd) o theorems "" [(("", []), args)]; -fun apply_theorems_i args = apfst (List.concat o map snd) o theorems_i "" [(("", []), args)]; +fun apply_theorems args = apfst (maps snd) o theorems "" [(("", []), args)]; +fun apply_theorems_i args = apfst (maps snd) o theorems_i "" [(("", []), args)]; fun smart_theorems kind NONE args thy = thy |> theorems kind args diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Isar/local_syntax.ML --- a/src/Pure/Isar/local_syntax.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/Isar/local_syntax.ML Thu Apr 27 15:06:35 2006 +0200 @@ -104,7 +104,7 @@ let val mixfixes' = mixfixes |> fold (add_mixfix prmode) (filter_out mixfix_struct decls); val fixes' = fold (fn (((x, true), _), _) => cons x | _ => I) mixfixes' []; - val structs' = structs @ List.mapPartial prep_struct decls; + val structs' = structs @ map_filter prep_struct decls; in build_syntax thy (mixfixes', (structs', fixes')) end); end; diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/Isar/locale.ML Thu Apr 27 15:06:35 2006 +0200 @@ -201,7 +201,7 @@ (* registrations that subsume t *) fun subsumers thy t regs = - List.filter (fn (t', _) => Pattern.matches thy (t', t)) (Termtab.dest regs); + filter (fn (t', _) => Pattern.matches thy (t', t)) (Termtab.dest regs); (* look up registration, pick one that subsumes the query *) fun lookup sign (regs, ts) = @@ -235,7 +235,7 @@ in (case subs of [] => let val sups = - List.filter (fn (t', _) => Pattern.matches sign (t, t')) (Termtab.dest regs); + filter (fn (t', _) => Pattern.matches sign (t, t')) (Termtab.dest regs); val sups' = map (apfst untermify) sups in (Termtab.update (t, (attn, [])) regs, sups') end | _ => (regs, [])) @@ -480,7 +480,7 @@ val thy = ProofContext.theory_of ctxt; fun prt_id (name, parms) = [Pretty.block (Pretty.breaks (map Pretty.str (extern thy name :: parms)))]; - val prt_ids = List.concat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids)); + val prt_ids = flat (separate [Pretty.str " +", Pretty.brk 1] (map prt_id ids)); val err_msg = if forall (equal "" o #1) ids then msg else msg ^ "\n" ^ Pretty.string_of (Pretty.block @@ -537,19 +537,19 @@ | unify _ env = env; val (unifier, _) = fold unify (Ts' ~~ Us') (Vartab.empty, maxidx''); val Vs = map (Option.map (Envir.norm_type unifier)) Us'; - val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (List.mapPartial I Vs)); + val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map_filter I Vs)); in map (Option.map (Envir.norm_type unifier')) Vs end; -fun params_of elemss = distinct (eq_fst (op =)) (List.concat (map (snd o fst) elemss)); -fun params_of' elemss = distinct (eq_fst (op =)) (List.concat (map (snd o fst o fst) elemss)); +fun params_of elemss = distinct (eq_fst (op =)) (maps (snd o fst) elemss); +fun params_of' elemss = distinct (eq_fst (op =)) (maps (snd o fst o fst) elemss); fun params_syn_of syn elemss = - distinct (eq_fst (op =)) (List.concat (map (snd o fst) elemss)) |> + distinct (eq_fst (op =)) (maps (snd o fst) elemss) |> map (apfst (fn x => (x, the (Symtab.lookup syn x)))); (* CB: param_types has the following type: ('a * 'b option) list -> ('a * 'b) list *) -fun param_types ps = List.mapPartial (fn (_, NONE) => NONE | (x, SOME T) => SOME (x, T)) ps; +fun param_types ps = map_filter (fn (_, NONE) => NONE | (x, SOME T) => SOME (x, T)) ps; fun merge_syntax ctxt ids ss = Symtab.merge (op =) ss @@ -577,7 +577,7 @@ fun unique_parms ctxt elemss = let val param_decls = - List.concat (map (fn (((name, (ps, qs)), _), _) => map (rpair (name, ps)) qs) elemss) + maps (fn (((name, (ps, qs)), _), _) => map (rpair (name, ps)) qs) elemss |> Symtab.make_list |> Symtab.dest; in (case find_first (fn (_, ids) => length ids > 1) param_decls of @@ -594,7 +594,7 @@ fun varify i = Term.map_type_tfree (fn (a, S) => TVar ((a, i), S)); fun varify_parms (i, ps) = map (apsnd (varify i)) (param_types ps); - val parms = fixed_parms @ List.concat (map varify_parms idx_parmss); + val parms = fixed_parms @ maps varify_parms idx_parmss; fun unify T U envir = Sign.typ_unify thy (U, T) envir handle Type.TUNIFY => @@ -611,8 +611,8 @@ val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms')); fun inst_parms (i, ps) = - foldr Term.add_typ_tfrees [] (List.mapPartial snd ps) - |> List.mapPartial (fn (a, S) => + foldr Term.add_typ_tfrees [] (map_filter snd ps) + |> map_filter (fn (a, S) => let val T = Envir.norm_type unifier' (TVar ((a, i), S)) in if T = TFree (a, S) then NONE else SOME (a, T) end) |> Symtab.make; @@ -716,7 +716,7 @@ val new_ids' = map (fn (id, ths) => (id, ([], Derived ths))) (new_ids ~~ new_ths); in - fold add_regs new_idTs (ths @ List.concat new_ths, ids @ new_ids') + fold add_regs new_idTs (ths @ flat new_ths, ids @ new_ids') end; (* distribute top-level axioms over assumed ids *) @@ -724,10 +724,10 @@ fun axiomify all_ps ((name, parms), (_, Assumed _)) axioms = let val {elems, ...} = the_locale thy name; - val ts = List.concat (map - (fn (Assumes asms, _) => List.concat (map (map #1 o #2) asms) + val ts = maps + (fn (Assumes asms, _) => maps (map #1 o #2) asms | _ => []) - elems); + elems; val (axs1, axs2) = chop (length ts) axioms; in (((name, parms), (all_ps, Assumed axs1)), axs2) end | axiomify all_ps (id, (_, Derived ths)) axioms = @@ -762,7 +762,7 @@ handle ERROR msg => err_in_locale' ctxt msg ids'; val ids'' = distinct (eq_fst (op =)) (map (rename_parms top ren) ids'); - val parms'' = distinct (op =) (List.concat (map (#2 o #1) ids'')); + val parms'' = distinct (op =) (maps (#2 o #1) ids''); val syn'' = syn' |> Symtab.dest |> map (Element.rename_var ren) |> Symtab.make; (* check for conflicting syntax? *) in (ids'', parms'', syn'') end @@ -849,7 +849,7 @@ | activate_elem _ ((ctxt, Assumed axs), Assumes asms) = let val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms; - val ts = List.concat (map (map #1 o #2) asms'); + val ts = maps (map #1 o #2) asms'; val (ps, qs) = chop (length ts) axs; val (_, ctxt') = ctxt |> fold ProofContext.fix_frees ts @@ -895,7 +895,7 @@ fold_map (fn (((name, ps), mode), raw_elems) => fn ctxt => let val elems = map (prep_facts ctxt) raw_elems; - val (ctxt', res) = apsnd List.concat + val (ctxt', res) = apsnd flat (activate_elems (((name, ps), mode), elems) ctxt); val elems' = elems |> map (Element.map_ctxt {name = I, var = I, typ = I, term = I, fact = I, attrib = Args.closure}); @@ -916,7 +916,7 @@ fun activate_facts prep_facts (ctxt, args) = let val ((elemss, factss), ctxt') = activate_elemss prep_facts args ctxt |>> split_list - in (ctxt', (elemss, List.concat factss)) end; + in (ctxt', (elemss, flat factss)) end; end; @@ -1047,7 +1047,7 @@ fold ProofContext.declare_term (map Free fixed_params) ctxt; val int_elemss = raw_elemss - |> List.mapPartial (fn (id, Int es) => SOME (id, es) | _ => NONE) + |> map_filter (fn (id, Int es) => SOME (id, es) | _ => NONE) |> unify_elemss ctxt_with_fixed fixed_params; val (_, raw_elemss') = foldl_map (fn ((_, es) :: elemss, (id, Int _)) => (elemss, (id, Int es)) | x => x) @@ -1086,7 +1086,7 @@ | eval_text _ (_, Assumed _) is_ext (Assumes asms) (((exts, exts'), (ints, ints')), (xs, env, defs)) = let - val ts = List.concat (map (map #1 o #2) asms); + val ts = maps (map #1 o #2) asms; val ts' = map (norm_term env) ts; val spec' = if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints')) @@ -1165,7 +1165,7 @@ val [(id' as (_, mode), es)] = unify_elemss ctxt parms [(id, e)]; val wits' = case mode of Assumed _ => wits | Derived ths => wits @ ths; val text' = fold (eval_text ctxt id' false) es text; - val es' = List.mapPartial + val es' = map_filter (finish_derived (ProofContext.theory_of ctxt) wits' mode) es; in ((text', wits'), (id', map Int es')) end | finish_elems ctxt parms do_close ((text, wits), ((id, Ext e), [propp])) = @@ -1214,7 +1214,7 @@ val (ctxt, all_propp) = prepp (fold ProofContext.declare_term (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp); (* CB: add type information from conclusion and external elements to context *) - val ctxt = fold ProofContext.declare_term (List.concat (map (map fst) all_propp)) ctxt; + val ctxt = fold ProofContext.declare_term (maps (map fst) all_propp) ctxt; (* CB: resolve schematic variables (patterns) in conclusion and external elements. *) val all_propp' = map2 (curry (op ~~)) (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp)))) (map (map snd) all_propp); @@ -1307,9 +1307,9 @@ in elemss |> get |> map (fn (_, es) => map (fn Int e => e) es) - |> Library.flat - |> Library.mapfilter (fn Assumes asms => SOME asms | _ => NONE) - |> Library.flat + |> flat + |> map_filter (fn Assumes asms => SOME asms | _ => NONE) + |> flat |> map (apsnd (map fst)) end; @@ -1350,7 +1350,7 @@ val ((ids, syn), raw_elemsss) = foldl_map (flatten (context, prep_expr thy)) ((import_ids, import_syn), elements); - val raw_elemss = List.concat raw_elemsss; + val raw_elemss = flat raw_elemsss; (* CB: raw_import_elemss @ raw_elemss is the normalised list of context elements obtained from import and elements. *) val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close @@ -1368,9 +1368,8 @@ val (ctxt, (elemss, _)) = activate_facts prep_facts (import_ctxt, qs); val stmt = distinct Term.aconv - (List.concat (map (fn ((_, Assumed axs), _) => - List.concat (map (#hyps o Thm.rep_thm o #2) axs) - | ((_, Derived _), _) => []) qs)); + (maps (fn ((_, Assumed axs), _) => maps (#hyps o Thm.rep_thm o #2) axs + | ((_, Derived _), _) => []) qs); val cstmt = map (cterm_of thy) stmt; in ((((import_ctxt, import_elemss), (ctxt, elemss, syn)), (parms, spec, defs)), (cstmt, concl)) @@ -1411,7 +1410,7 @@ val (((_, import_elemss), (ctxt, elemss, _)), _) = read_context import body (ProofContext.init thy); val prt_elem = Element.pretty_ctxt ctxt; - val all_elems = List.concat (map #2 (import_elemss @ elemss)); + val all_elems = maps #2 (import_elemss @ elemss); in Pretty.big_list "locale elements:" (all_elems |> (if show_facts then I else filter (fn Notes _ => false | _ => true)) @@ -1456,7 +1455,7 @@ fun vinst_names ps = map (the o Symtab.lookup vinst) ps; val inst = Symtab.make (parms ~~ ts); val ids' = map (apsnd vinst_names) ids; - val wits = List.concat (map (snd o the o get_global_registration thy) ids'); + val wits = maps (snd o the o get_global_registration thy) ids'; in ((tinst, inst), wits) end; @@ -1468,7 +1467,7 @@ val parms = the_locale thy target |> #params |> map fst; val ids = flatten (ProofContext.init thy, intern_expr thy) (([], Symtab.empty), Expr (Locale target)) |> fst |> fst - |> List.mapPartial (fn (id, (_, Assumed _)) => SOME id | _ => NONE) + |> map_filter (fn (id, (_, Assumed _)) => SOME id | _ => NONE) val regs = get_global_registrations thy target; @@ -1598,7 +1597,7 @@ val (body, bodyT, body_eq) = atomize_spec thy norm_ts; val env = Term.add_term_free_names (body, []); - val xs = List.filter (fn (x, _) => x mem_string env) parms; + val xs = filter (fn (x, _) => x mem_string env) parms; val Ts = map #2 xs; val extraTs = (Term.term_tfrees body \\ foldr Term.add_typ_tfrees [] Ts) |> Library.sort_wrt #1 |> map TFree; @@ -1724,8 +1723,8 @@ fun axiomify axioms elemss = (axioms, elemss) |> foldl_map (fn (axs, (id, elems)) => let - val ts = List.concat (List.mapPartial (fn (Assumes asms) => - SOME (List.concat (map (map #1 o #2) asms)) | _ => NONE) elems); + val ts = flat (map_filter (fn (Assumes asms) => + SOME (maps (map #1 o #2) asms) | _ => NONE) elems); val (axs1, axs2) = chop (length ts) axs; in (axs2, ((id, Assumed axs1), elems)) end) |> snd; @@ -1734,7 +1733,7 @@ (pred_ctxt, axiomify predicate_axioms elemss'); val export = ProofContext.export_view predicate_statement ctxt thy_ctxt; val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])])); - val elems' = List.concat (map #2 (List.filter (equal "" o #1 o #1) elemss')); + val elems' = maps #2 (filter (equal "" o #1 o #1) elemss'); val thy' = pred_thy |> PureThy.note_thmss_qualified "" bname facts' |> snd @@ -1821,7 +1820,7 @@ curry (locale_results kind loc ((names ~~ loc_attss) ~~ loc_results)) loc_ctxt #-> (fn res => if name = "" andalso null loc_atts then I - else #2 o locale_results kind loc [((name, loc_atts), List.concat (map #2 res))]) + else #2 o locale_results kind loc [((name, loc_atts), maps #2 res)]) #> #2 #> after_qed loc_results results end; @@ -1863,7 +1862,7 @@ fun extract_asms_elem (Fixes _) ts = ts | extract_asms_elem (Constrains _) ts = ts | extract_asms_elem (Assumes asms) ts = - ts @ List.concat (map (fn (_, ams) => map (fn (t, _) => t) ams) asms) + ts @ maps (fn (_, ams) => map (fn (t, _) => t) ams) asms | extract_asms_elem (Defines defs) ts = ts @ map (fn (_, (def, _)) => def) defs | extract_asms_elem (Notes _) ts = ts; @@ -1907,7 +1906,7 @@ |> fold (fn (id, thms) => fold (add_wit id) thms) (map fst propss ~~ thmss); - val prems = List.concat (List.mapPartial + val prems = flat (map_filter (fn ((id, Assumed _), _) => Option.map snd (get_reg thy_ctxt' id) | ((_, Derived _), _) => NONE) all_elemss); val disch = satisfy_protected prems; @@ -1916,7 +1915,7 @@ val thy_ctxt'' = thy_ctxt' (* add witnesses of Derived elements *) |> fold (fn (id, thms) => fold (add_wit id o apsnd disch) thms) - (List.mapPartial (fn ((_, Assumed _), _) => NONE + (map_filter (fn ((_, Assumed _), _) => NONE | ((id, Derived thms), _) => SOME (id, thms)) all_elemss) in thy_ctxt'' @@ -1963,7 +1962,7 @@ val pvTs = map Type.varifyT pTs; (* instantiations given by user *) - val given = List.mapPartial (fn (_, (NONE, _)) => NONE + val given = map_filter (fn (_, (NONE, _)) => NONE | (x, (SOME inst, T)) => SOME (x, (inst, T))) (ps ~~ (insts ~~ pvTs)); val (given_ps, given_insts) = split_list given; val tvars = foldr Term.add_typ_tvars [] pvTs; @@ -1992,7 +1991,7 @@ val inst = Symtab.make (given_ps ~~ map rename vs); (* defined params without user input *) - val not_given = List.mapPartial (fn (x, (NONE, T)) => SOME (x, T) + val not_given = map_filter (fn (x, (NONE, T)) => SOME (x, T) | (_, (SOME _, _)) => NONE) (ps ~~ (insts ~~ pTs)); fun add_def (p, pT) inst = let @@ -2018,7 +2017,7 @@ (Element.inst_term insts t, Element.inst_thm thy insts th))) mode))); (* remove fragments already registered with theory or context *) - val new_inst_elemss = List.filter (fn ((id, _), _) => + val new_inst_elemss = filter (fn ((id, _), _) => not (test_reg thy_ctxt id)) inst_elemss; val new_ids = map #1 new_inst_elemss; @@ -2072,11 +2071,11 @@ the target, unless already present - add facts of induced registrations to theory **) - val t_ids = List.mapPartial + val t_ids = map_filter (fn (id, (_, Assumed _)) => SOME id | _ => NONE) target_ids; fun activate thmss thy = let - val satisfy = satisfy_protected (List.concat thmss); + val satisfy = satisfy_protected (flat thmss); val ids_elemss_thmss = ids_elemss ~~ thmss; val regs = get_global_registrations thy target; @@ -2090,7 +2089,7 @@ fun inst_parms ps = map (the o AList.lookup (op =) (map #1 fixed ~~ vts)) ps; val disch = satisfy_protected wits; - val new_elemss = List.filter (fn (((name, ps), _), _) => + val new_elemss = filter (fn (((name, ps), _), _) => not (test_global_registration thy (name, inst_parms ps))) (ids_elemss); fun activate_assumed_id (((_, Derived _), _), _) thy = thy | activate_assumed_id ((((name, ps), Assumed _), _), thms) thy = let diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/Isar/method.ML Thu Apr 27 15:06:35 2006 +0200 @@ -265,7 +265,7 @@ let val rules = if not (null arg_rules) then arg_rules - else List.concat (ContextRules.find_rules false facts goal ctxt) + else flat (ContextRules.find_rules false facts goal ctxt) in trace ctxt rules; tac rules facts i end); fun meth tac x = METHOD (HEADGOAL o tac x); @@ -617,7 +617,7 @@ local fun sect ss = Scan.first (map Scan.lift ss); -fun thms ss = Scan.repeat (Scan.unless (sect ss) Attrib.multi_thm) >> List.concat; +fun thms ss = Scan.repeat (Scan.unless (sect ss) Attrib.multi_thm) >> flat; fun app (f, att) (context, ths) = foldl_map att (Context.map_proof f context, ths); diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Isar/obtain.ML --- a/src/Pure/Isar/obtain.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/Isar/obtain.ML Thu Apr 27 15:06:35 2006 +0200 @@ -119,7 +119,7 @@ (*obtain asms*) val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms); - val asm_props = List.concat (map (map fst) proppss); + val asm_props = maps (map fst) proppss; val asms = map fst (Attrib.map_specs (prep_att thy) raw_asms) ~~ proppss; val _ = ProofContext.warn_extra_tfrees fix_ctxt asms_ctxt; @@ -131,9 +131,9 @@ fun occs_var x = Library.get_first (fn t => Term.find_free t (ProofContext.get_skolem fix_ctxt x)) asm_props; val raw_parms = map occs_var xs; - val parms = List.mapPartial I raw_parms; + val parms = map_filter I raw_parms; val parm_names = - List.mapPartial (fn (SOME (Free a), x) => SOME (a, x) | _ => NONE) (raw_parms ~~ xs); + map_filter (fn (SOME (Free a), x) => SOME (a, x) | _ => NONE) (raw_parms ~~ xs); val that_name = if name = "" then thatN else name; val that_prop = @@ -284,7 +284,7 @@ val names = cases |> map_index (fn (i, ("", _)) => string_of_int (i + 1) | (_, (name, _)) => name); val elems = cases |> map (fn (_, (vars, _)) => - Element.Constrains (vars |> List.mapPartial (fn (x, SOME T) => SOME (x, T) | _ => NONE))); + Element.Constrains (vars |> map_filter (fn (x, SOME T) => SOME (x, T) | _ => NONE))); val concl = cases |> map (fn (_, (_, props)) => (("", []), map (rpair ([], [])) props)); fun mk_stmt stmt ctxt = diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Isar/outer_parse.ML --- a/src/Pure/Isar/outer_parse.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/Isar/outer_parse.ML Thu Apr 27 15:06:35 2006 +0200 @@ -262,11 +262,11 @@ val params = Scan.repeat1 name -- Scan.option ($$$ "::" |-- !!! typ) >> (fn (xs, T) => map (rpair T) xs); -val simple_fixes = and_list1 params >> List.concat; +val simple_fixes = and_list1 params >> flat; val fixes = and_list1 (name -- Scan.option ($$$ "::" |-- typ) -- mixfix >> (single o triple1) || - params >> map Syntax.no_syn) >> List.concat; + params >> map Syntax.no_syn) >> flat; (* terms *) @@ -311,7 +311,7 @@ ((Scan.repeat1 (Scan.repeat1 (atom_arg is_symid blk) || paren_args "(" ")" (args is_symid) || - paren_args "[" "]" (args is_symid))) >> List.concat) x; + paren_args "[" "]" (args is_symid))) >> flat) x; val arguments = args T.is_sid false; @@ -350,7 +350,7 @@ val locale_fixes = and_list1 (name -- Scan.option ($$$ "::" |-- typ) -- locale_mixfix >> (single o triple1) || - params >> map Syntax.no_syn) >> List.concat; + params >> map Syntax.no_syn) >> flat; local @@ -401,7 +401,7 @@ val obtain_case = parname -- (Scan.optional (simple_fixes --| $$$ "where") [] -- - (and_list1 (Scan.repeat1 prop) >> List.concat)); + (and_list1 (Scan.repeat1 prop) >> flat)); val general_statement = statement >> (fn x => ([], Element.Shows x)) || diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/Isar/outer_syntax.ML Thu Apr 27 15:06:35 2006 +0200 @@ -197,10 +197,10 @@ |> Source.source T.stopper (Scan.bulk (P.$$$ "--" -- P.!!! P.text >> K NONE || P.not_eof >> SOME)) (if do_recover then SOME recover else NONE) - |> Source.mapfilter I + |> Source.map_filter I |> Source.source T.stopper (Scan.bulk (fn xs => P.!!! (command term do_trace (cmd ())) xs)) (if do_recover then SOME recover else NONE) - |> Source.mapfilter I + |> Source.map_filter I end; diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/Isar/proof.ML Thu Apr 27 15:06:35 2006 +0200 @@ -237,7 +237,7 @@ put_thms_internal (AutoBind.thisN, facts); fun these_factss more_facts (named_factss, state) = - (named_factss, state |> put_facts (SOME (List.concat (map snd named_factss) @ more_facts))); + (named_factss, state |> put_facts (SOME (maps snd named_factss @ more_facts))); fun export_facts inner outer = (case get_facts inner of @@ -655,7 +655,7 @@ state' |> map_goal I (fn (statement, using, goal, before_qed, after_qed) => let val ctxt = context_of state'; - val ths = List.concat (map snd named_facts); + val ths = maps snd named_facts; in (statement, f ctxt ths using, g ctxt ths goal, before_qed, after_qed) end)); fun append_using _ ths using = using @ ths; @@ -794,7 +794,7 @@ |> enter_forward |> open_block |> map_context_result (fn ctxt => swap (prepp (ctxt, raw_propp))); - val props = List.concat propss; + val props = flat propss; val goal = Goal.init (Thm.cterm_of thy (Logic.mk_conjunction_list2 propss)); val after_qed' = after_qed |>> (fn after_local => @@ -823,7 +823,7 @@ val outer_ctxt = context_of outer_state; val props = - List.concat stmt + flat stmt |> ProofContext.generalize goal_ctxt outer_ctxt; val results = stmt @@ -874,7 +874,7 @@ #> global_results kind ((names ~~ attss) ~~ res) #-> (fn res' => (print_results thy_ctxt ((kind, name), res') : unit; - #2 o global_results kind [((name, atts), List.concat (map #2 res'))])) + #2 o global_results kind [((name, atts), maps #2 res')])) #> Sign.restore_naming thy; fun after_qed' results = @@ -961,7 +961,7 @@ |> capture; fun after_qed' results = - refine_goals print_rule (context_of state) (List.concat results) + refine_goals print_rule (context_of state) (flat results) #> Seq.maps (after_qed results); in state diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/Isar/proof_context.ML Thu Apr 27 15:06:35 2006 +0200 @@ -280,8 +280,8 @@ val fixed_names_of = map #2 o fixes_of; val assumptions_of = #1 o #assms o rep_context; -val assms_of = map Thm.term_of o List.concat o map #1 o assumptions_of; -val prems_of = List.concat o map #2 o #2 o #assms o rep_context; +val assms_of = map Thm.term_of o maps #1 o assumptions_of; +val prems_of = maps #2 o #2 o #assms o rep_context; val binds_of = #binds o rep_context; @@ -778,7 +778,7 @@ let val thy = Thm.theory_of_thm rule; val prop = Thm.full_prop_of rule; - val frees = map (Thm.cterm_of thy) (List.mapPartial (Term.find_free prop) fixes); + val frees = map (Thm.cterm_of thy) (map_filter (Term.find_free prop) fixes); val tfrees = gen (Term.add_term_tfree_names (prop, [])); in rule @@ -849,7 +849,7 @@ then () else fail (); fun norm_bind (xi, (_, t)) = if member (op =) domain xi then SOME (xi, Envir.norm_term env t) else NONE; - in List.mapPartial norm_bind (Envir.alist_of env) end; + in map_filter norm_bind (Envir.alist_of env) end; (* add_binds(_i) *) @@ -889,7 +889,7 @@ let val ts = prep_terms ctxt (map snd raw_binds); val (binds, ctxt') = - apfst List.concat (fold_map (prep_bind prep_pats) (map fst raw_binds ~~ ts) ctxt); + apfst flat (fold_map (prep_bind prep_pats) (map fst raw_binds ~~ ts) ctxt); val binds' = if gen then map #1 binds ~~ generalize ctxt' ctxt (map #2 binds) else binds; @@ -922,7 +922,7 @@ in ((prop, chop (length raw_pats1) pats), (ctxt', props)) end | prep _ _ = sys_error "prep_propp"; val (propp, (context', _)) = (fold_map o fold_map) prep args - (context, prep_props schematic context (List.concat (map (map fst) args))); + (context, prep_props schematic context (maps (map fst) args)); in (context', propp) end; fun matches ctxt (prop, (pats1, pats2)) = @@ -931,7 +931,7 @@ fun gen_bind_propp prepp (ctxt, raw_args) = let val (ctxt', args) = prepp (ctxt, raw_args); - val binds = List.concat (List.concat (map (map (matches ctxt')) args)); + val binds = flat (flat (map (map (matches ctxt')) args)); val propss = map (map #1) args; (*generalize result: context evaluated now, binds added later*) @@ -1061,7 +1061,7 @@ let val (ct', th') = foldl_map (Thm.proof_attributes (attrs @ more_attrs)) (ct, get ctxt th) in (ct', th' :: ths) end; val (ctxt', rev_thms) = fold app ths_attrs (ctxt, []); - val thms = List.concat (rev rev_thms); + val thms = flat (rev rev_thms); in ((name, thms), ctxt' |> put_thms true (name, SOME thms)) end); in @@ -1245,7 +1245,7 @@ val (propss, ctxt1) = swap (prepp (ctxt, map snd args)); val (results, ctxt2) = fold_map gen_assm (map fst args ~~ propss) ctxt1; - val new_asms = List.concat (map #1 results); + val new_asms = maps #1 results; val new_prems = map #2 results; val ctxt3 = ctxt2 |> map_assms (fn (asms, prems) => (asms @ [(new_asms, exp)], prems @ new_prems)) @@ -1428,13 +1428,13 @@ fun prt_sect _ _ _ [] = [] | prt_sect s sep prt xs = [Pretty.block (Pretty.breaks (Pretty.str s :: - List.concat (Library.separate sep (map (Library.single o prt) xs))))]; + flat (Library.separate sep (map (Library.single o prt) xs))))]; fun prt_case (name, (fixes, (asms, (lets, cs)))) = Pretty.block (Pretty.fbreaks (Pretty.str (name ^ ":") :: prt_sect "fix" [] (Pretty.str o fst) fixes @ prt_sect "let" [Pretty.str "and"] prt_let - (List.mapPartial (fn (xi, SOME t) => SOME (xi, t) | _ => NONE) lets) @ + (map_filter (fn (xi, SOME t) => SOME (xi, t) | _ => NONE) lets) @ (if forall (null o #2) asms then [] else prt_sect "assume" [Pretty.str "and"] prt_asm asms) @ prt_sect "subcases:" [] (Pretty.str o fst) cs)); diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Isar/proof_display.ML --- a/src/Pure/Isar/proof_display.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/Isar/proof_display.ML Thu Apr 27 15:06:35 2006 +0200 @@ -62,7 +62,7 @@ local fun pretty_facts ctxt = - List.concat o (separate [Pretty.fbrk, Pretty.str "and "]) o + flat o (separate [Pretty.fbrk, Pretty.str "and "]) o map (single o ProofContext.pretty_fact ctxt); fun pretty_results ctxt ((kind, ""), facts) = @@ -76,7 +76,7 @@ fun name_results "" res = res | name_results name res = let - val n = length (List.concat (map snd res)); + val n = length (maps snd res); fun name_res (a, ths) i = let val m = length ths; diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Isar/rule_cases.ML --- a/src/Pure/Isar/rule_cases.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/Isar/rule_cases.ML Thu Apr 27 15:06:35 2006 +0200 @@ -107,7 +107,7 @@ else abs fixes1 (app (map (Term.dummy_pattern o #2) fixes2) (abs fixes2 t)); val (assumes1, assumes2) = extract_assumes (NameSpace.qualified name) case_outline prop - |> pairself (map (apsnd (List.concat o map Logic.dest_conjunctions))); + |> pairself (map (apsnd (maps Logic.dest_conjunctions))); val concl = ObjectLogic.drop_judgment thy (Logic.strip_assums_concl prop); val binds = @@ -272,7 +272,7 @@ | _ => []); fun save_case_concls th = - let val concls = Thm.tags_of_thm th |> List.mapPartial + let val concls = Thm.tags_of_thm th |> map_filter (fn (a, b :: cs) => if a = case_concl_tagN then SOME (b, cs) else NONE | _ => NONE) diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/Proof/extraction.ML Thu Apr 27 15:06:35 2006 +0200 @@ -307,7 +307,7 @@ let val {realizes_eqns, typeof_eqns, defs, types, ...} = ExtractionData.get thy; - val procs = List.concat (map (fst o snd) types); + val procs = maps (fst o snd) types; val rtypes = map fst types; val eqns = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns); val thy' = add_syntax thy; @@ -343,7 +343,7 @@ val thy' = add_syntax thy; val {realizes_eqns, typeof_eqns, defs, types, ...} = ExtractionData.get thy'; - val procs = List.concat (map (fst o snd) types); + val procs = maps (fst o snd) types; val eqns = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns); val prop' = Pattern.rewrite_term thy' (map (Logic.dest_equals o prop_of) defs) [] prop; @@ -460,7 +460,7 @@ val thy' = add_syntax thy; val {realizes_eqns, typeof_eqns, types, realizers, defs, expand, prep} = ExtractionData.get thy; - val procs = List.concat (map (fst o snd) types); + val procs = maps (fst o snd) types; val rtypes = map fst types; val typroc = typeof_proc (Sign.defaultS thy'); val prep = the_default (K I) prep thy' o ProofRewriteRules.elim_defs thy' false defs o diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Proof/proof_rewrite_rules.ML --- a/src/Pure/Proof/proof_rewrite_rules.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/Proof/proof_rewrite_rules.ML Thu Apr 27 15:06:35 2006 +0200 @@ -246,11 +246,11 @@ val f = if not r then I else let val cnames = map (fst o dest_Const o fst) defs'; - val thms = List.concat (map (fn (s, ps) => + val thms = maps (fn (s, ps) => if s mem defnames then [] else map (pair s o SOME o fst) (filter_out (fn (p, _) => null (term_consts p inter cnames)) ps)) - (Symtab.dest (thms_of_proof prf Symtab.empty))) + (Symtab.dest (thms_of_proof prf Symtab.empty)) in Reconstruct.expand_proof thy thms end in rewrite_terms (Pattern.rewrite_term thy defs' []) diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Proof/reconstruct.ML --- a/src/Pure/Proof/reconstruct.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/Proof/reconstruct.ML Thu Apr 27 15:06:35 2006 +0200 @@ -110,7 +110,7 @@ fun decompose sg Ts (env, p as (t, u)) = let fun rigrig (a, T) (b, U) uT ts us = if a <> b then cantunify sg p - else apsnd List.concat (foldl_map (decompose sg Ts) (uT env T U, ts ~~ us)) + else apsnd flat (foldl_map (decompose sg Ts) (uT env T U, ts ~~ us)) in case pairself (strip_comb o Envir.head_norm env) p of ((Const c, ts), (Const d, us)) => rigrig c d (unifyT sg) ts us | ((Free c, ts), (Free d, us)) => rigrig c d (unifyT sg) ts us diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Syntax/lexicon.ML --- a/src/Pure/Syntax/lexicon.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/Syntax/lexicon.ML Thu Apr 27 15:06:35 2006 +0200 @@ -279,7 +279,7 @@ Scan.one Symbol.is_blank >> K NONE; in (case Scan.error (Scan.finite Symbol.stopper (Scan.repeat scan_token)) chs of - (toks, []) => List.mapPartial I toks @ [EndToken] + (toks, []) => map_filter I toks @ [EndToken] | (_, cs) => error ("Inner lexical error at: " ^ quote (implode cs))) end; diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Syntax/mixfix.ML --- a/src/Pure/Syntax/mixfix.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/Syntax/mixfix.ML Thu Apr 27 15:06:35 2006 +0200 @@ -183,7 +183,7 @@ | _ => error ("Bad mixfix declaration for type: " ^ quote t)) end; - val mfix = List.mapPartial mfix_of type_decls; + val mfix = map_filter mfix_of type_decls; val xconsts = map name_of type_decls; in SynExt.syn_ext mfix xconsts ([], [], [], []) [] ([], []) end; @@ -224,9 +224,9 @@ fun binder (c, _, Binder (sy, _, _)) = SOME (sy, c) | binder _ = NONE; - val mfix = List.concat (map mfix_of const_decls); + val mfix = maps mfix_of const_decls; val xconsts = map name_of const_decls; - val binders = List.mapPartial binder const_decls; + val binders = map_filter binder const_decls; val binder_trs = binders |> map (SynExt.stamp_trfun binder_stamp o apsnd K o SynTrans.mk_binder_tr); val binder_trs' = binders |> map (SynExt.stamp_trfun binder_stamp o diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/Syntax/parser.ML Thu Apr 27 15:06:35 2006 +0200 @@ -418,7 +418,7 @@ map prod_of_chain ((these o AList.lookup (op =) chains) tag); in map (pretty_prod name) nt_prods end; - in List.concat (map pretty_nt taglist) end; + in maps pretty_nt taglist end; (** Operations on gramars **) @@ -840,12 +840,12 @@ end; val nts = - List.mapPartial (fn (_, _, _, Nonterminal (a, prec) :: _, _, _) => + map_filter (fn (_, _, _, Nonterminal (a, prec) :: _, _, _) => SOME (a, prec) | _ => NONE) (Array.sub (stateset, i-1)); val allowed = distinct (op =) (get_starts nts [] @ - (List.mapPartial (fn (_, _, _, Terminal a :: _, _, _) => SOME a + (map_filter (fn (_, _, _, Terminal a :: _, _, _) => SOME a | _ => NONE) (Array.sub (stateset, i-1)))); in syntax_error (if prev_token = EndToken then indata @@ -862,7 +862,7 @@ end)); -fun get_trees l = List.mapPartial (fn (_, _, [pt], _, _, _) => SOME pt | _ => NONE) +fun get_trees l = map_filter (fn (_, _, [pt], _, _, _) => SOME pt | _ => NONE) l; fun earley prods tags chains startsymbol indata = diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Syntax/printer.ML --- a/src/Pure/Syntax/printer.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/Syntax/printer.ML Thu Apr 27 15:06:35 2006 +0200 @@ -192,7 +192,7 @@ type prtabs = (string * ((symb list * int * int) list) Symtab.table) list; fun mode_tab prtabs mode = the_default Symtab.empty (AList.lookup (op =) prtabs mode); -fun mode_tabs prtabs modes = List.mapPartial (AList.lookup (op =) prtabs) (modes @ [""]); +fun mode_tabs prtabs modes = map_filter (AList.lookup (op =) prtabs) (modes @ [""]); (* xprod_to_fmt *) @@ -244,7 +244,7 @@ fun change_prtabs f mode xprods prtabs = let - val fmts = List.mapPartial xprod_to_fmt xprods; + val fmts = map_filter xprod_to_fmt xprods; val tab = fold f fmts (mode_tab prtabs mode); in AList.update (op =) (mode, tab) prtabs end; diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Syntax/syn_ext.ML --- a/src/Pure/Syntax/syn_ext.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/Syntax/syn_ext.ML Thu Apr 27 15:06:35 2006 +0200 @@ -218,7 +218,7 @@ $$ "'" -- Scan.one Symbol.is_blank >> K NONE; val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (~$$ "'"); -val read_symbs = List.mapPartial I o the o Scan.read Symbol.stopper scan_symbs; +val read_symbs = map_filter I o the o Scan.read Symbol.stopper scan_symbs; fun unique_index xsymbs = if length (List.filter is_index xsymbs) <= 1 then xsymbs @@ -360,7 +360,7 @@ print_ast_translation) = trfuns; val (xprods, parse_rules') = map (mfix_to_xprod convert is_logtype) mfixes - |> split_list |> apsnd (rev o List.concat); + |> split_list |> apsnd (rev o flat); val mfix_consts = distinct (op =) (map (fn Mfix x => #3 x) mfixes @ map (fn XProd x => #3 x) xprods); in diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Syntax/syn_trans.ML --- a/src/Pure/Syntax/syn_trans.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/Syntax/syn_trans.ML Thu Apr 27 15:06:35 2006 +0200 @@ -467,8 +467,8 @@ | ast_of (Parser.Tip tok) = Ast.Variable (Lexicon.str_of_token tok); val exn_results = map (capture ast_of) pts; - val exns = List.mapPartial get_exn exn_results; - val results = List.mapPartial get_result exn_results + val exns = map_filter get_exn exn_results; + val results = map_filter get_result exn_results in (case (results, exns) of ([], exn :: _) => raise exn | _ => results) end; @@ -500,8 +500,8 @@ | t => t); val exn_results = map (capture (term_of #> free_fixed)) asts; - val exns = List.mapPartial get_exn exn_results; - val results = List.mapPartial get_result exn_results + val exns = map_filter get_exn exn_results; + val results = map_filter get_result exn_results in (case (results, exns) of ([], exn :: _) => raise exn | _ => results) end; end; diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/Syntax/syntax.ML Thu Apr 27 15:06:35 2006 +0200 @@ -114,8 +114,7 @@ (** tables of token translation functions **) fun lookup_tokentr tabs modes = - let val trs = distinct (eq_fst (op =)) - (List.concat (map (these o AList.lookup (op =) tabs) (modes @ [""]))) + let val trs = distinct (eq_fst (op =)) (maps (these o AList.lookup (op =) tabs) (modes @ [""])) in fn c => Option.map fst (AList.lookup (op =) trs c) end; fun merge_tokentrtabs tabs1 tabs2 = @@ -150,7 +149,7 @@ type ruletab = (Ast.ast * Ast.ast) list Symtab.table; -fun dest_ruletab tab = List.concat (map snd (Symtab.dest tab)); +fun dest_ruletab tab = maps snd (Symtab.dest tab); (* empty, extend, merge ruletabs *) @@ -474,8 +473,8 @@ fun prep_rules rd_pat raw_rules = let val rules = map (map_trrule rd_pat) raw_rules in - (map check_rule (List.mapPartial parse_rule rules), - map check_rule (List.mapPartial print_rule rules)) + (map check_rule (map_filter parse_rule rules), + map check_rule (map_filter print_rule rules)) end in diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Thy/thm_database.ML --- a/src/Pure/Thy/thm_database.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/Thy/thm_database.ML Thu Apr 27 15:06:35 2006 +0200 @@ -104,7 +104,7 @@ fun mk_thm (bname, xname, singleton) = "val " ^ bname ^ " = thm" ^ (if singleton then "" else "s") ^ " " ^ quote xname; in - Symtab.keys thms |> List.mapPartial prune + Symtab.keys thms |> map_filter prune |> Symtab.make_list |> Symtab.dest |> sort_wrt #1 |> map (fn (prfx, entries) => entries |> sort_wrt #1 |> map mk_thm |> cat_lines |> mk_struct prfx) diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/Thy/thy_info.ML Thu Apr 27 15:06:35 2006 +0200 @@ -157,7 +157,7 @@ NONE => [] | SOME {master, files, ...} => (case master of SOME m => [#1 (ThyLoad.get_thy m)] | NONE => []) @ - (List.mapPartial (Option.map #1 o #2) files)); + (map_filter (Option.map #1 o #2) files)); fun get_preds name = (thy_graph Graph.imm_preds name) handle Graph.UNDEF _ => @@ -222,7 +222,7 @@ in fun touch_thys names = - List.app outdate_thy (thy_graph Graph.all_succs (List.mapPartial check_unfinished names)); + List.app outdate_thy (thy_graph Graph.all_succs (map_filter check_unfinished names)); fun touch_thy name = touch_thys [name]; fun touch_child_thys name = touch_thys (thy_graph Graph.imm_succs name); @@ -298,7 +298,7 @@ else #1 (ThyLoad.deps_thy dir name ml); val files = get_files name; - val missing_files = List.mapPartial (fn (path, NONE) => SOME (Path.pack path) | _ => NONE) files; + val missing_files = map_filter (fn (path, NONE) => SOME (Path.pack path) | _ => NONE) files; in if null missing_files then () else warning (loader_msg "unresolved dependencies of theory" [name] ^ @@ -434,7 +434,7 @@ val deps = if known_thy name then get_deps name else (init_deps NONE (map #1 uses)); (*records additional ML files only!*) - val uses_now = List.mapPartial (fn (x, true) => SOME x | _ => NONE) uses; + val uses_now = map_filter (fn (x, true) => SOME x | _ => NONE) uses; val _ = change_thys (update_node name bparents (deps, SOME (Theory.copy theory))); val theory' = theory |> present dir' name bparents uses; @@ -470,7 +470,7 @@ fun get_variant (x, y_name) = if Theory.eq_thy (x, get_theory y_name) then NONE else SOME y_name; - val variants = List.mapPartial get_variant (parents ~~ parent_names); + val variants = map_filter get_variant (parents ~~ parent_names); fun register G = (Graph.new_node (name, (NONE, SOME theory)) G diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Tools/am_compiler.ML --- a/src/Pure/Tools/am_compiler.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/Tools/am_compiler.ML Thu Apr 27 15:06:35 2006 +0200 @@ -113,7 +113,7 @@ | remove_dups [] = [] fun constants_of PVar = [] - | constants_of (PConst (c, ps)) = c :: List.concat (map constants_of ps) + | constants_of (PConst (c, ps)) = c :: maps constants_of ps fun constants_of_term (Var _) = [] | constants_of_term (Abs m) = constants_of_term m @@ -133,7 +133,7 @@ "structure "^name^" = struct", "", "datatype term = App of term * term | Abs of term | Var of int | Const of int | Closure of term list * term"] - val constants = remove_dups (List.concat (map (fn (p, r) => ((constants_of p)@(constants_of_term r))) prog)) + val constants = remove_dups (maps (fn (p, r) => ((constants_of p)@(constants_of_term r))) prog) val _ = map (fn x => write (" | c"^(str x))) constants val _ = writelist [ "", diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Tools/class_package.ML --- a/src/Pure/Tools/class_package.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/Tools/class_package.ML Thu Apr 27 15:06:35 2006 +0200 @@ -177,7 +177,7 @@ fun the_intros thy = let val gr = (fst o fst o ClassData.get) thy; - in (List.mapPartial (#intro o rep_classdata o Graph.get_node gr) o Graph.keys) gr end; + in (map_filter (#intro o rep_classdata o Graph.get_node gr) o Graph.keys) gr end; fun subst_clsvar v ty_subst = map_type_tfree (fn u as (w, _) => diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Tools/codegen_package.ML --- a/src/Pure/Tools/codegen_package.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/Tools/codegen_package.ML Thu Apr 27 15:06:35 2006 +0200 @@ -164,14 +164,14 @@ NameSpace.drop_base c'; val c'' = NameSpace.append prefix (NameSpace.base c'); fun mangle (Type (tyco, tys)) = - (NameSpace.base o alias_get thy) tyco :: flat (List.mapPartial mangle tys) |> SOME + (NameSpace.base o alias_get thy) tyco :: flat (map_filter mangle tys) |> SOME | mangle _ = NONE in Vartab.empty |> Type.raw_match (Sign.the_const_type thy c, ty) |> map (snd o snd) o Vartab.dest - |> List.mapPartial mangle + |> map_filter mangle |> flat |> null ? K ["x"] |> cons c'' diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Tools/codegen_serializer.ML --- a/src/Pure/Tools/codegen_serializer.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/Tools/codegen_serializer.ML Thu Apr 27 15:06:35 2006 +0200 @@ -322,7 +322,7 @@ then SOME eq else (warning ("in function " ^ quote name ^ ", throwing away one " ^ "non-executable function clause"); NONE) - in case List.mapPartial check_eq eqs + in case map_filter check_eq eqs of [] => error ("in function " ^ quote name ^ ", no" ^ "executable function clauses found") | eqs => (name, (eqs, ty)) @@ -666,13 +666,13 @@ val (ml_from_funs, ml_from_datatypes) = ml_fun_datatyp (is_cons, needs_type) (tyco_syntax, const_syntax) resolv; val filter_datatype = - List.mapPartial + map_filter (fn (name, CodegenThingol.Datatype info) => SOME (name, info) | (name, CodegenThingol.Datatypecons _) => NONE | (name, def) => error ("datatype block containing illegal def: " ^ (Pretty.output o CodegenThingol.pretty_def) def)); fun filter_class defs = - case List.mapPartial + case map_filter (fn (name, CodegenThingol.Class info) => SOME (name, info) | (name, CodegenThingol.Classmember _) => NONE | (name, def) => error ("class block containing illegal def: " @@ -1085,7 +1085,7 @@ | hs_from_def (_, CodegenThingol.Classinstmember) = NONE in - case List.mapPartial (fn (name, def) => hs_from_def (name, def)) defs + case map_filter (fn (name, def) => hs_from_def (name, def)) defs of [] => NONE | l => (SOME o Pretty.chunks o separate (str "")) l end; diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Tools/codegen_theorems.ML --- a/src/Pure/Tools/codegen_theorems.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/Tools/codegen_theorems.ML Thu Apr 27 15:06:35 2006 +0200 @@ -429,7 +429,7 @@ fun get_funs thy (c, ty) = let - val filter_typ = Library.mapfilter (fn ((_, ty'), thm) => + val filter_typ = map_filter (fn ((_, ty'), thm) => if Sign.typ_instance thy (ty', ty) orelse Sign.typ_instance thy (ty, ty') then SOME thm else debug_msg (fn _ => "dropping " ^ string_of_thm thm) NONE); diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Tools/codegen_thingol.ML --- a/src/Pure/Tools/codegen_thingol.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/Tools/codegen_thingol.ML Thu Apr 27 15:06:35 2006 +0200 @@ -503,7 +503,7 @@ Pretty.str ("module " ^ name ^ " {") :: Pretty.brk 1 :: Pretty.chunks (map pretty (AList.make (Graph.get_node modl) - (Graph.strong_conn modl |> List.concat |> rev))) + (Graph.strong_conn modl |> flat |> rev))) :: Pretty.str "}" :: nil ) | pretty (name, Def def) = @@ -533,7 +533,7 @@ in modl |> Graph.strong_conn - |> List.concat + |> flat |> rev |> map one_node |> Pretty.chunks @@ -1121,7 +1121,7 @@ val name_qual = NameSpace.pack (prfx @ [name]) in (name_qual, resolver prfx name_qual) end; fun mk_contents prfx module = - List.mapPartial (seri prfx) + map_filter (seri prfx) ((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module) and seri prfx ([(name, Module modl)]) = seri_module (resolver []) (map (resolver []) (imports_of module (prfx @ [name]))) @@ -1131,7 +1131,7 @@ (map (fn (name, Def def) => (fst (mk_name prfx name), def)) ds) in seri_module (resolver []) (imports_of module []) - (*map (resolver []) (Graph.strong_conn module |> List.concat |> rev)*) + (*map (resolver []) (Graph.strong_conn module |> flat |> rev)*) (("", name_root), (mk_contents [] module)) end; diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Tools/compute.ML --- a/src/Pure/Tools/compute.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/Tools/compute.ML Thu Apr 27 15:06:35 2006 +0200 @@ -24,7 +24,7 @@ exception Make of string; -fun is_mono_typ (Type (_, list)) = List.all is_mono_typ list +fun is_mono_typ (Type (_, list)) = forall is_mono_typ list | is_mono_typ _ = false fun is_mono_term (Const (_, t)) = is_mono_typ t @@ -247,9 +247,8 @@ let val (_, {mk_rews={mk=mk,mk_eq_True=emk, ...},...}) = rep_ss (simpset_of thy) fun mk_eq_True th = (case emk th of NONE => [th] | SOME th' => [th, th']) - fun app f l = List.concat (map f l) in - basic_make thy (app mk (app mk_eq_True ths)) + basic_make thy (maps mk (maps mk_eq_True ths)) end fun compute (Computer r) naming ct = diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/Tools/nbe_codegen.ML --- a/src/Pure/Tools/nbe_codegen.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/Tools/nbe_codegen.ML Thu Apr 27 15:06:35 2006 +0200 @@ -131,8 +131,7 @@ val globals = map lookup (filter defined funs); val default_eqn = ([params], S.app Eval_Constr (S.tup[S.quote nm,params])); val code = S.eqns (MLname nm) - (Library.flat(map (mk_eqn defined nm ar) eqns) - @ [default_eqn]) + (maps (mk_eqn defined nm ar) eqns @ [default_eqn]) val register = tab_update (S.app Eval_mk_Fun (S.tup[S.quote nm, MLname nm, string_of_int ar])) in diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/axclass.ML --- a/src/Pure/axclass.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/axclass.ML Thu Apr 27 15:06:35 2006 +0200 @@ -267,7 +267,7 @@ (* definition *) - val conjs = map (curry Logic.mk_inclass (Term.aT [])) super @ List.concat axiomss; + val conjs = map (curry Logic.mk_inclass (Term.aT [])) super @ flat axiomss; val class_eq = Logic.mk_equals (Logic.mk_inclass (Term.aT [], class), Logic.mk_conjunction_list conjs); diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/codegen.ML --- a/src/Pure/codegen.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/codegen.ML Thu Apr 27 15:06:35 2006 +0200 @@ -442,8 +442,7 @@ | (true, "isup") => "" :: check_str zs | (ctrl, s') => (if ctrl then "ctrl_" ^ s' else s') :: check_str zs) | (ys, zs) => implode ys :: check_str zs); - val s' = space_implode "_" - (List.concat (map (check_str o Symbol.explode) (NameSpace.unpack s))) + val s' = space_implode "_" (maps (check_str o Symbol.explode) (NameSpace.unpack s)) in if Symbol.is_ascii_letter (hd (explode s')) then s' else "id_" ^ s' end; @@ -537,7 +536,7 @@ val names = foldr add_term_names (map (fst o fst) (Drule.vars_of_terms ts)) ts; val reserved = names inter ThmDatabase.ml_reserved; - val (illegal, alt_names) = split_list (List.mapPartial (fn s => + val (illegal, alt_names) = split_list (map_filter (fn s => let val s' = mk_id s in if s = s' then NONE else SOME (s, s') end) names) val ps = (reserved @ illegal) ~~ variantlist (map (suffix "'") reserved @ alt_names, names); @@ -564,7 +563,7 @@ fun get_assoc_code thy s T = Option.map snd (Library.find_first (fn ((s', T'), _) => s = s' andalso is_instance thy T T') (#consts (CodegenData.get thy))); -fun get_aux_code xs = List.mapPartial (fn (m, code) => +fun get_aux_code xs = map_filter (fn (m, code) => if m = "" orelse m mem !mode then SOME code else NONE) xs; fun mk_deftab thy = @@ -841,7 +840,7 @@ fun output_code gr module xs = let - val code = List.mapPartial (fn s => + val code = map_filter (fn s => let val c as (_, module', _) = Graph.get_node gr s in if module = "" orelse module = module' then SOME (s, c) else NONE end) (rev (Graph.all_preds gr xs)); @@ -859,9 +858,9 @@ val modules = distinct (op =) (map (#2 o snd) code); val mod_gr = foldr (uncurry Graph.add_edge_acyclic) (foldr (uncurry (Graph.new_node o rpair ())) Graph.empty modules) - (List.concat (map (fn (s, (_, module, _)) => map (pair module) + (maps (fn (s, (_, module, _)) => map (pair module) (filter_out (equal module) (map (#2 o Graph.get_node gr) - (Graph.imm_succs gr s)))) code)); + (Graph.imm_succs gr s)))) code); val modules' = rev (Graph.all_preds mod_gr (map (#2 o Graph.get_node gr) xs)) in @@ -896,13 +895,13 @@ val (gr', ps) = foldl_map (fn (gr, (s, t)) => apsnd (pair s) (invoke_codegen thy defs "" module false (gr, t))) (gr, map (apsnd (expand o preprocess_term thy o prep_term thy)) xs); - val code = List.mapPartial + val code = map_filter (fn ("", _) => NONE | (s', p) => SOME (Pretty.string_of (Pretty.block [Pretty.str ("val " ^ s' ^ " ="), Pretty.brk 1, p, Pretty.str ";"]))) ps; val code' = space_implode "\n\n" code ^ "\n\n"; val code'' = - List.mapPartial (fn (name, s) => + map_filter (fn (name, s) => if "library" mem !mode andalso name = module andalso null code then NONE else SOME (name, mk_struct name s)) @@ -923,7 +922,7 @@ val strip_tname = implode o tl o explode; fun pretty_list xs = Pretty.block (Pretty.str "[" :: - List.concat (separate [Pretty.str ",", Pretty.brk 1] (map single xs)) @ + flat (separate [Pretty.str ",", Pretty.brk 1] (map single xs)) @ [Pretty.str "]"]); fun mk_type p (TVar ((s, i), _)) = Pretty.str @@ -940,8 +939,8 @@ (Pretty.block (separate (Pretty.brk 1) (Pretty.str (mk_qual_id module (get_type_id' (fn s' => "term_of_" ^ s') s gr)) :: - List.concat (map (fn T => - [mk_term_of gr module true T, mk_type true T]) Ts)))); + maps (fn T => + [mk_term_of gr module true T, mk_type true T]) Ts))); (**** Test data generators ****) @@ -985,7 +984,7 @@ Pretty.brk 1, Pretty.str "then NONE", Pretty.brk 1, Pretty.str "else ", Pretty.block [Pretty.str "SOME ", Pretty.block (Pretty.str "[" :: - List.concat (separate [Pretty.str ",", Pretty.brk 1] + flat (separate [Pretty.str ",", Pretty.brk 1] (map (fn ((s, T), s') => [Pretty.block [Pretty.str ("(" ^ Library.quote (Symbol.escape s) ^ ","), Pretty.brk 1, mk_app false (mk_term_of gr "Generated" false T) diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/consts.ML --- a/src/Pure/consts.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/consts.ML Thu Apr 27 15:06:35 2006 +0200 @@ -67,7 +67,7 @@ make_consts (f (decls, constraints, rev_abbrevs, expand_abbrevs)); fun abbrevs_of (Consts ({rev_abbrevs, ...}, _)) modes = - List.concat (map (Symtab.lookup_list rev_abbrevs) modes); + maps (Symtab.lookup_list rev_abbrevs) modes; (* dest consts *) diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/context.ML --- a/src/Pure/context.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/context.ML Thu Apr 27 15:06:35 2006 +0200 @@ -380,7 +380,7 @@ let val parents = maximal_thys (distinct eq_thy (map check_thy imports)); - val ancestors = distinct eq_thy (parents @ List.concat (map ancestors_of parents)); + val ancestors = distinct eq_thy (parents @ maps ancestors_of parents); val Theory ({id, ids, iids, ...}, data, _, _) = (case parents of [] => error "No parent theories" diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/defs.ML --- a/src/Pure/defs.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/defs.ML Thu Apr 27 15:06:35 2006 +0200 @@ -69,7 +69,7 @@ in (consts', specified') end); fun specifications_of (Defs {specified, ...}) c = - (List.mapPartial + (map_filter (fn (_, (false, _, _, _)) => NONE | (_, (true, specname, thyname, ty)) => SOME (ty, (specname, thyname))) o Inttab.dest o the_default Inttab.empty o Symtab.lookup specified) c; diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/display.ML --- a/src/Pure/display.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/display.ML Thu Apr 27 15:06:35 2006 +0200 @@ -188,7 +188,7 @@ if not syn then NONE else SOME (prt_typ (Type (t, []))); - val pretty_arities = List.concat o map (fn (t, ars) => map (prt_arity t) ars); + val pretty_arities = maps (fn (t, ars) => map (prt_arity t) ars); fun pretty_const (c, ty) = Pretty.block [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty]; @@ -208,8 +208,8 @@ val tdecls = NameSpace.dest_table types; val arties = NameSpace.dest_table (Sign.type_space thy, arities); val cnsts = NameSpace.extern_table constants; - val log_cnsts = List.mapPartial (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts; - val abbrevs = List.mapPartial (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts; + val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts; + val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts; val cnstrs = NameSpace.extern_table constraints; val axms = NameSpace.extern_table axioms; val oras = NameSpace.extern_table oracles; @@ -221,8 +221,8 @@ Pretty.big_list "classes:" (map pretty_classrel clsses), pretty_default default, pretty_witness witness, - Pretty.big_list "syntactic types:" (List.mapPartial (pretty_type true) tdecls), - Pretty.big_list "logical types:" (List.mapPartial (pretty_type false) tdecls), + Pretty.big_list "syntactic types:" (map_filter (pretty_type true) tdecls), + Pretty.big_list "logical types:" (map_filter (pretty_type false) tdecls), Pretty.big_list "type arities:" (pretty_arities arties), Pretty.big_list "logical consts:" (map pretty_const log_cnsts), Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs), diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/drule.ML --- a/src/Pure/drule.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/drule.ML Thu Apr 27 15:06:35 2006 +0200 @@ -534,7 +534,7 @@ fun thas RLN (i,thbs) = let val resolve = biresolution false (map (pair false) thas) i fun resb thb = Seq.list_of (resolve thb) handle THM _ => [] - in List.concat (map resb thbs) end; + in maps resb thbs end; fun thas RL thbs = thas RLN (1,thbs); @@ -961,8 +961,8 @@ let fun err msg = raise TYPE ("instantiate': " ^ msg, - List.mapPartial (Option.map Thm.typ_of) cTs, - List.mapPartial (Option.map Thm.term_of) cts); + map_filter (Option.map Thm.typ_of) cTs, + map_filter (Option.map Thm.term_of) cts); fun inst_of (v, ct) = (Thm.cterm_of (Thm.theory_of_cterm ct) (Var v), ct) diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/goal.ML --- a/src/Pure/goal.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/goal.ML Thu Apr 27 15:06:35 2006 +0200 @@ -123,7 +123,7 @@ val frees = Term.add_frees statement []; val fixed_frees = filter_out (member (op =) xs o #1) frees; val fixed_tfrees = fold (Term.add_tfreesT o #2) fixed_frees []; - val params = List.mapPartial (fn x => Option.map (pair x) (AList.lookup (op =) frees x)) xs; + val params = map_filter (fn x => Option.map (pair x) (AList.lookup (op =) frees x)) xs; fun err msg = cat_error msg ("The error(s) above occurred for the goal statement:\n" ^ diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/meta_simplifier.ML --- a/src/Pure/meta_simplifier.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/meta_simplifier.ML Thu Apr 27 15:06:35 2006 +0200 @@ -398,7 +398,7 @@ fun rewrite_rule_extra_vars prems elhs erhs = not (term_varnames erhs subset fold add_term_varnames prems (term_varnames elhs)) orelse - not (term_tvars erhs subset (term_tvars elhs union List.concat (map term_tvars prems))); + not (term_tvars erhs subset (term_tvars elhs union maps term_tvars prems)); (*simple test for looping rewrite rules and stupid orientations*) fun default_reorient thy prems lhs rhs = @@ -488,16 +488,16 @@ end; fun extract_rews (Simpset (_, {mk_rews = {mk, ...}, ...}), thms) = - List.concat (map (fn thm => map (rpair (Thm.name_of_thm thm)) (mk thm)) thms); + maps (fn thm => map (rpair (Thm.name_of_thm thm)) (mk thm)) thms; fun orient_comb_simps comb mk_rrule (ss, thms) = let val rews = extract_rews (ss, thms); - val rrules = List.concat (map mk_rrule rews); + val rrules = maps mk_rrule rews; in Library.foldl comb (ss, rrules) end; fun extract_safe_rrules (ss, thm) = - List.concat (map (orient_rrule ss) (extract_rews (ss, [thm]))); + maps (orient_rrule ss) (extract_rews (ss, [thm])); (*add rewrite rules explicitly; do not reorient!*) fun ss addsimps thms = @@ -570,7 +570,7 @@ raise SIMPLIFIER ("Congruence must start with a constant", thm); val (alist, _) = congs; val alist2 = List.filter (fn (x, _) => x <> a) alist; - val weak2 = alist2 |> List.mapPartial (fn (a, {thm, ...}: cong) => + val weak2 = alist2 |> map_filter (fn (a, {thm, ...}: cong) => if is_full_cong thm then NONE else SOME a); in ((alist2, weak2), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end); @@ -1037,7 +1037,7 @@ in (extract_safe_rrules (ss, asm), SOME asm) end and add_rrules (rrss, asms) ss = - Library.foldl (insert_rrule true) (ss, List.concat rrss) |> add_prems (List.mapPartial I asms) + Library.foldl (insert_rrule true) (ss, flat rrss) |> add_prems (map_filter I asms) and disch r (prem, eq) = let diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/net.ML --- a/src/Pure/net.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/net.ML Thu Apr 27 15:06:35 2006 +0200 @@ -197,7 +197,7 @@ | _ => rands t (net, var::nets) (*var could match also*) end; -fun extract_leaves l = List.concat (map (fn Leaf(xs) => xs) l); +fun extract_leaves l = maps (fn Leaf xs => xs) l; (*return items whose key could match t, WHICH MUST BE BETA-ETA NORMAL*) fun match_term net t = @@ -236,7 +236,7 @@ | dest (Net {comb, var, atoms}) = map (cons_fst CombK) (dest comb) @ map (cons_fst VarK) (dest var) @ - List.concat (map (fn (a, net) => map (cons_fst (AtomK a)) (dest net)) (Symtab.dest atoms)); + maps (fn (a, net) => map (cons_fst (AtomK a)) (dest net)) (Symtab.dest atoms); fun merge eq (net1, net2) = fold (insert_safe eq) (dest net2) net1; diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/pattern.ML --- a/src/Pure/pattern.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/pattern.ML Thu Apr 27 15:06:35 2006 +0200 @@ -177,7 +177,7 @@ let val js = ints_of' env ts; val js' = map (try (trans d)) js; val ks = mk_proj_list js'; - val ls = List.mapPartial I js' + val ls = map_filter I js' val Hty = type_of_G env (Fty,length js,ks) val (env',H) = Envir.genvar a (env,Hty) val env'' = diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/proof_general.ML --- a/src/Pure/proof_general.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/proof_general.ML Thu Apr 27 15:06:35 2006 +0200 @@ -493,7 +493,7 @@ in fun setup_present_hook () = - Present.add_hook (fn _ => fn res => tell_thm_deps (List.concat (map #2 res))); + Present.add_hook (fn _ => fn res => tell_thm_deps (maps #2 res)); end; @@ -1456,7 +1456,7 @@ "\n '(" ^ space_implode "\n " (map (quote o regexp_quote) strs) ^ "))\n"; fun make_elisp_commands commands kind = defconst kind - (commands |> List.mapPartial (fn (c, _, k, _) => if k = kind then SOME c else NONE)); + (commands |> map_filter (fn (c, _, k, _) => if k = kind then SOME c else NONE)); fun make_elisp_syntax (keywords, commands) = ";;\n\ diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/proofterm.ML Thu Apr 27 15:06:35 2006 +0200 @@ -414,15 +414,15 @@ (**** substitutions ****) fun del_conflicting_tvars envT T = Term.instantiateT - (List.mapPartial (fn ixnS as (_, S) => + (map_filter (fn ixnS as (_, S) => (Type.lookup (envT, ixnS); NONE) handle TYPE _ => SOME (ixnS, TFree ("'dummy", S))) (typ_tvars T)) T; fun del_conflicting_vars env t = Term.instantiate - (List.mapPartial (fn ixnS as (_, S) => + (map_filter (fn ixnS as (_, S) => (Type.lookup (type_env env, ixnS); NONE) handle TYPE _ => SOME (ixnS, TFree ("'dummy", S))) (term_tvars t), - List.mapPartial (fn Var (ixnT as (_, T)) => + map_filter (fn Var (ixnT as (_, T)) => (Envir.lookup (env, ixnT); NONE) handle TYPE _ => SOME (ixnT, Free ("dummy", T))) (term_vars t)) t; @@ -836,7 +836,7 @@ fun add_funvars Ts (vs, t) = if is_fun (fastype_of1 (Ts, t)) then - vs union List.mapPartial (fn Var (ixn, T) => + vs union map_filter (fn Var (ixn, T) => if is_fun T then SOME ixn else NONE | _ => NONE) (vars_of t) else vs; @@ -903,7 +903,7 @@ in (b, is, ch, if ch then Abst (a, Option.map compress_typ T, body') else prf) end | shrink ls lev (prf as AbsP (a, t, body)) = let val (b, is, ch, body') = shrink (lev::ls) lev body - in (b orelse member (op =) is 0, List.mapPartial (fn 0 => NONE | i => SOME (i-1)) is, + in (b orelse member (op =) is 0, map_filter (fn 0 => NONE | i => SOME (i-1)) is, ch, if ch then AbsP (a, Option.map compress_term t, body') else prf) end | shrink ls lev prf = diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/pure_thy.ML Thu Apr 27 15:06:35 2006 +0200 @@ -219,7 +219,7 @@ error ("Bad subscript " ^ string_of_int i ^ " for " ^ quote name ^ " (length " ^ string_of_int n ^ ")") else List.nth (thms, i - 1); - in map select (List.concat (map (interval n) is)) end; + in map select (maps (interval n) is) end; (* selections *) @@ -263,7 +263,7 @@ |> the_thms name |> select_thm thmref |> map (Thm.transfer theory) end; -fun get_thmss thy thmrefs = List.concat (map (get_thms thy) thmrefs); +fun get_thmss thy thmrefs = maps (get_thms thy) thmrefs; fun get_thm thy thmref = single_thm (name_of_thmref thmref) (get_thms thy thmref); fun thm name = get_thm (the_context ()) (Name name); @@ -279,14 +279,13 @@ fun thms_containing theory spec = (theory :: Theory.ancestors_of theory) - |> map (fn thy => + |> maps (fn thy => FactIndex.find (fact_index_of thy) spec |> List.filter (fn (name, ths) => valid_thms theory (Name name, ths)) - |> distinct (eq_fst (op =))) - |> List.concat; + |> distinct (eq_fst (op =))); fun thms_containing_consts thy consts = - thms_containing thy (consts, []) |> map #2 |> List.concat + thms_containing thy (consts, []) |> maps #2 |> map (fn th => (Thm.name_of_thm th, th)); @@ -294,9 +293,9 @@ fun thms_of thy = let val thms = #2 (theorems_of thy) - in map (fn th => (Thm.name_of_thm th, th)) (List.concat (map snd (Symtab.dest thms))) end; + in map (fn th => (Thm.name_of_thm th, th)) (maps snd (Symtab.dest thms)) end; -fun all_thms_of thy = List.concat (map thms_of (thy :: Theory.ancestors_of thy)); +fun all_thms_of thy = maps thms_of (thy :: Theory.ancestors_of thy); @@ -379,7 +378,7 @@ let fun app (x, (ths, atts)) = foldl_map (Thm.theory_attributes atts) (x, ths); val (thms, thy') = thy |> enter_thms - name_thmss (name_thms false) (apsnd List.concat o foldl_map app) + name_thmss (name_thms false) (apsnd flat o foldl_map app) (bname, map (fn (ths, atts) => (get thy ths, atts @ more_atts @ [kind k])) ths_atts); in ((bname, thms), thy') end); diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/search.ML --- a/src/Pure/search.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/search.ML Thu Apr 27 15:06:35 2006 +0200 @@ -243,7 +243,7 @@ ([],[]) => [] | ([],nonsats) => (message("breadth=" ^ string_of_int(length nonsats)); - bfs (List.concat (map tacf nonsats))) + bfs (maps tacf nonsats)) | (sats,_) => sats) in (fn st => Seq.of_list (bfs [st])) end; diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/sign.ML --- a/src/Pure/sign.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/sign.ML Thu Apr 27 15:06:35 2006 +0200 @@ -345,7 +345,7 @@ fun mapping add_names f t = let fun f' x = let val y = f x in if x = y then NONE else SOME (x, y) end; - val tab = List.mapPartial f' (add_names t []); + val tab = map_filter f' (add_names t []); fun get x = the_default x (AList.lookup (op =) tab x); in get end; @@ -385,7 +385,7 @@ fun pretty_typ thy T = Syntax.pretty_typ (Context.Theory thy) (syn_of thy) (extern_typ thy T); fun pretty_sort thy S = Syntax.pretty_sort (Context.Theory thy) (syn_of thy) (extern_sort thy S); -fun pretty_classrel thy cs = Pretty.block (List.concat +fun pretty_classrel thy cs = Pretty.block (flat (separate [Pretty.str " <", Pretty.brk 1] (map (single o pretty_sort thy o single) cs))); fun pretty_arity thy (a, Ss, S) = @@ -597,8 +597,8 @@ handle TYPE (msg, _, _) => Exn (ERROR msg); val err_results = map infer termss; - val errs = List.mapPartial (fn Exn (ERROR msg) => SOME msg | _ => NONE) err_results; - val results = List.mapPartial get_result err_results; + val errs = map_filter (fn Exn (ERROR msg) => SOME msg | _ => NONE) err_results; + val results = map_filter get_result err_results; val ambiguity = length termss; fun ambig_msg () = @@ -614,7 +614,7 @@ \You may still want to disambiguate your grammar or your input." else (); hd results) else (cat_error (ambig_msg ()) ("More than one term is type correct:\n" ^ - cat_lines (map (Pretty.string_of_term pp) (List.concat (map fst results))))) + cat_lines (map (Pretty.string_of_term pp) (maps fst results)))) end; fun infer_types pp thy consts def_type def_sort used freeze tsT = diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/sorts.ML --- a/src/Pure/sorts.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/sorts.ML Thu Apr 27 15:06:35 2006 +0200 @@ -248,7 +248,7 @@ | check_result (SOME (T, S)) = if of_sort (classes, arities) (T, S) then SOME (T, S) else sys_error ("Sorts.witness_sorts: bad witness for sort " ^ str_of_sort S); - in List.mapPartial check_result (#2 (witness_aux (classes, arities) log_types hyps sorts)) end; + in map_filter check_result (#2 (witness_aux (classes, arities) log_types hyps sorts)) end; end; diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/tactic.ML --- a/src/Pure/tactic.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/tactic.ML Thu Apr 27 15:06:35 2006 +0200 @@ -462,8 +462,7 @@ (fn (prem,i) => let val hyps = Logic.strip_assums_hyp prem and concl = Logic.strip_assums_concl prem - val kbrls = Net.unify_term inet concl @ - List.concat (map (Net.unify_term enet) hyps) + val kbrls = Net.unify_term inet concl @ maps (Net.unify_term enet) hyps in PRIMSEQ (biresolution match (order kbrls) i) end); (*versions taking pre-built nets. No filtering of brls*) diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/theory.ML --- a/src/Pure/theory.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/theory.ML Thu Apr 27 15:06:35 2006 +0200 @@ -144,7 +144,7 @@ val oracle_space = #1 o #oracles o rep_theory; val axioms_of = Symtab.dest o #2 o #axioms o rep_theory; -fun all_axioms_of thy = List.concat (map axioms_of (thy :: ancestors_of thy)); +fun all_axioms_of thy = maps axioms_of (thy :: ancestors_of thy); val defs_of = #defs o rep_theory; diff -r a6205c6203ea -r 9f11af8f7ef9 src/Pure/type_infer.ML --- a/src/Pure/type_infer.ML Thu Apr 27 12:11:56 2006 +0200 +++ b/src/Pure/type_infer.ML Thu Apr 27 15:06:35 2006 +0200 @@ -413,7 +413,7 @@ (*collect result unifier*) fun ch_var (xi, Link (r as ref (Param S))) = (r := PTVar (xi, S); NONE) | ch_var xi_T = SOME xi_T; - val env = List.mapPartial ch_var Tps; + val env = map_filter ch_var Tps; (*convert back to terms/typs*) val mk_var =