--- 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? *)
--- 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*)
--- 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
--- 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;
--- 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;
--- 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 ",";
--- 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);
--- 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 --
--- 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;
--- 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) = []
--- 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;
--- 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);
--- 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;
--- 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)
--- 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)));
--- 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));
--- 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
--- 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;
--- 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
--- 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);
--- 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 =
--- 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)) ||
--- 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;
--- 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
--- 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));
--- 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;
--- 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)
--- 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
--- 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' [])
--- 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
--- 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;
--- 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
--- 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 =
--- 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;
--- 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
--- 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;
--- 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
--- 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)
--- 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
--- 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 [
"",
--- 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, _) =>
--- 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''
--- 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;
--- 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);
--- 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;
--- 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 =
--- 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
--- 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);
--- 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 "<Top>" 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)
--- 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 *)
--- 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"
--- 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;
--- 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),
--- 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)
--- 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" ^
--- 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
--- 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;
--- 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'' =
--- 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\
--- 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 =
--- 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);
--- 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;
--- 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 =
--- 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;
--- 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*)
--- 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;
--- 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 =