replaced String.concat by implode;
replaced String.concatWith by space_implode;
replaced (Seq.flat o Seq.map) by Seq.maps;
replaced List.mapPartial by map_filter;
replaced List.concat by flat;
replaced (flat o map) by maps, which produces less garbage;
--- a/src/FOL/simpdata.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/FOL/simpdata.ML Thu Oct 15 23:28:10 2009 +0200
@@ -46,7 +46,7 @@
(case head_of p of
Const(a,_) =>
(case AList.lookup (op =) pairs a of
- SOME(rls) => List.concat (map atoms ([th] RL rls))
+ SOME(rls) => maps atoms ([th] RL rls)
| NONE => [th])
| _ => [th])
| _ => [th])
--- a/src/FOLP/simp.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/FOLP/simp.ML Thu Oct 15 23:28:10 2009 +0200
@@ -432,8 +432,8 @@
fun add_asms(ss,thm,a,anet,ats,cs) =
let val As = strip_varify(nth_subgoal i thm, a, []);
val thms = map (trivial o cterm_of(Thm.theory_of_thm thm)) As;
- val new_rws = List.concat(map mk_rew_rules thms);
- val rwrls = map mk_trans (List.concat(map mk_rew_rules thms));
+ val new_rws = maps mk_rew_rules thms;
+ val rwrls = map mk_trans (maps mk_rew_rules thms);
val anet' = List.foldr lhs_insert_thm anet rwrls
in if !tracing andalso not(null new_rws)
then writeln (cat_lines
@@ -589,7 +589,7 @@
val T' = Logic.incr_tvar 9 T;
in mk_cong_type thy (Const(f,T'),T') end;
-fun mk_congs thy = List.concat o map (mk_cong_thy thy);
+fun mk_congs thy = maps (mk_cong_thy thy);
fun mk_typed_congs thy =
let
@@ -599,7 +599,7 @@
val t = case Sign.const_type thy f of
SOME(_) => Const(f,T) | NONE => Free(f,T)
in (t,T) end
-in List.concat o map (mk_cong_type thy o readfT) end;
+in maps (mk_cong_type thy o readfT) end;
end;
end;
--- a/src/HOL/Import/xml.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Import/xml.ML Thu Oct 15 23:28:10 2009 +0200
@@ -137,7 +137,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 =
($$ "<" |-- scan_id --
--- a/src/HOL/Nominal/nominal_atoms.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Thu Oct 15 23:28:10 2009 +0200
@@ -851,7 +851,7 @@
val cps' =
let fun cps'_fun ak1 ak2 =
if ak1=ak2 then NONE else SOME (PureThy.get_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst"))
- in map (fn aki => (List.mapPartial I (map (cps'_fun aki) ak_names))) ak_names end;
+ in map (fn aki => (map_filter I (map (cps'_fun aki) ak_names))) ak_names end;
(* list of all dj_inst-theorems *)
val djs =
let fun djs_fun ak1 ak2 =
@@ -999,7 +999,7 @@
prm_cons_thms ~~ prm_inst_thms ~~
map (fn ths => Symtab.make (full_ak_names ~~ ths)) cp_thms ~~
map (fn thss => Symtab.make
- (List.mapPartial (fn (s, [th]) => SOME (s, th) | _ => NONE)
+ (map_filter (fn (s, [th]) => SOME (s, th) | _ => NONE)
(full_ak_names ~~ thss))) dj_thms))) thy33
end;
--- a/src/HOL/Nominal/nominal_datatype.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Thu Oct 15 23:28:10 2009 +0200
@@ -45,18 +45,18 @@
local
fun dt_recs (DtTFree _) = []
- | dt_recs (DtType (_, dts)) = List.concat (map dt_recs dts)
+ | dt_recs (DtType (_, dts)) = maps dt_recs dts
| dt_recs (DtRec i) = [i];
fun dt_cases (descr: descr) (_, args, constrs) =
let
fun the_bname i = Long_Name.base_name (#1 (valOf (AList.lookup (op =) descr i)));
- val bnames = map the_bname (distinct op = (List.concat (map dt_recs args)));
+ val bnames = map the_bname (distinct op = (maps dt_recs args));
in map (fn (c, _) => space_implode "_" (Long_Name.base_name c :: bnames)) constrs end;
fun induct_cases descr =
- DatatypeProp.indexify_names (List.concat (map (dt_cases descr) (map #2 descr)));
+ DatatypeProp.indexify_names (maps (dt_cases descr) (map #2 descr));
fun exhaust_cases descr i = dt_cases descr (valOf (AList.lookup (op =) descr i));
@@ -331,7 +331,7 @@
val _ = warning "perm_empty_thms";
- val perm_empty_thms = List.concat (map (fn a =>
+ val perm_empty_thms = maps (fn a =>
let val permT = mk_permT (Type (a, []))
in map standard (List.take (split_conj_thm
(Goal.prove_global thy2 [] []
@@ -347,7 +347,7 @@
ALLGOALS (asm_full_simp_tac (global_simpset_of thy2))])),
length new_type_names))
end)
- atoms);
+ atoms;
(**** prove (pi1 @ pi2) \<bullet> t = pi1 \<bullet> (pi2 \<bullet> t) ****)
@@ -357,7 +357,7 @@
val at_pt_inst = PureThy.get_thm thy2 "at_pt_inst";
val pt2 = PureThy.get_thm thy2 "pt2";
- val perm_append_thms = List.concat (map (fn a =>
+ val perm_append_thms = maps (fn a =>
let
val permT = mk_permT (Type (a, []));
val pi1 = Free ("pi1", permT);
@@ -381,7 +381,7 @@
(fn _ => EVERY [indtac induct perm_indnames 1,
ALLGOALS (asm_full_simp_tac (global_simpset_of thy2 addsimps [pt2', pt2_ax]))]))),
length new_type_names)
- end) atoms);
+ end) atoms;
(**** prove pi1 ~ pi2 ==> pi1 \<bullet> t = pi2 \<bullet> t ****)
@@ -390,7 +390,7 @@
val pt3 = PureThy.get_thm thy2 "pt3";
val pt3_rev = PureThy.get_thm thy2 "pt3_rev";
- val perm_eq_thms = List.concat (map (fn a =>
+ val perm_eq_thms = maps (fn a =>
let
val permT = mk_permT (Type (a, []));
val pi1 = Free ("pi1", permT);
@@ -417,7 +417,7 @@
(fn _ => EVERY [indtac induct perm_indnames 1,
ALLGOALS (asm_full_simp_tac (global_simpset_of thy2 addsimps [pt3', pt3_rev', pt3_ax]))]))),
length new_type_names)
- end) atoms);
+ end) atoms;
(**** prove pi1 \<bullet> (pi2 \<bullet> t) = (pi1 \<bullet> pi2) \<bullet> (pi1 \<bullet> t) ****)
@@ -506,7 +506,7 @@
val rep_set_names = DatatypeProp.indexify_names
(map (fn (i, _) => name_of_typ (nth_dtyp i) ^ "_set") descr);
val big_rep_name =
- space_implode "_" (DatatypeProp.indexify_names (List.mapPartial
+ space_implode "_" (DatatypeProp.indexify_names (map_filter
(fn (i, ("Nominal.noption", _, _)) => NONE
| (i, _) => SOME (name_of_typ (nth_dtyp i))) descr)) ^ "_set";
val _ = warning ("big_rep_name: " ^ big_rep_name);
@@ -521,8 +521,7 @@
| strip_option dt = ([], dt);
val dt_atomTs = distinct op = (map (typ_of_dtyp descr sorts)
- (List.concat (map (fn (_, (_, _, cs)) => List.concat
- (map (List.concat o map (fst o strip_option) o snd) cs)) descr)));
+ (maps (fn (_, (_, _, cs)) => maps (maps (fst o strip_option) o snd) cs) descr));
val dt_atoms = map (fst o dest_Type) dt_atomTs;
fun make_intr s T (cname, cargs) =
@@ -557,7 +556,7 @@
end;
val (intr_ts, (rep_set_names', recTs')) =
- apfst List.concat (apsnd ListPair.unzip (ListPair.unzip (List.mapPartial
+ apfst flat (apsnd ListPair.unzip (ListPair.unzip (map_filter
(fn ((_, ("Nominal.noption", _, _)), _) => NONE
| ((i, (_, _, constrs)), rep_set_name) =>
let val T = nth_dtyp i
@@ -582,7 +581,7 @@
val abs_perm = PureThy.get_thms thy4 "abs_perm";
- val perm_indnames' = List.mapPartial
+ val perm_indnames' = map_filter
(fn (x, (_, ("Nominal.noption", _, _))) => NONE | (x, _) => SOME x)
(perm_indnames ~~ descr);
@@ -861,8 +860,7 @@
perm_closed_thms @ Rep_thms)) 1)
end) Rep_thms;
- val perm_rep_perm_thms = List.concat (map prove_perm_rep_perm
- (atoms ~~ perm_closed_thmss));
+ val perm_rep_perm_thms = maps prove_perm_rep_perm (atoms ~~ perm_closed_thmss);
(* prove distinctness theorems *)
@@ -887,7 +885,7 @@
val perm_simps' = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) =>
let val T = nth_dtyp' i
- in List.concat (map (fn (atom, perm_closed_thms) =>
+ in maps (fn (atom, perm_closed_thms) =>
map (fn ((cname, dts), constr_rep_thm) =>
let
val cname = Sign.intern_const thy8
@@ -928,7 +926,7 @@
TRY (simp_tac (HOL_basic_ss addsimps
(perm_fun_def :: perm_defs @ Rep_thms @ Abs_inverse_thms @
perm_closed_thms)) 1)])
- end) (constrs ~~ constr_rep_thms)) (atoms ~~ perm_closed_thmss))
+ end) (constrs ~~ constr_rep_thms)) (atoms ~~ perm_closed_thmss)
end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss);
(** prove injectivity of constructors **)
@@ -943,7 +941,7 @@
val inject_thms = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) =>
let val T = nth_dtyp' i
- in List.mapPartial (fn ((cname, dts), constr_rep_thm) =>
+ in map_filter (fn ((cname, dts), constr_rep_thm) =>
if null dts then NONE else SOME
let
val cname = Sign.intern_const thy8
@@ -986,7 +984,7 @@
val (supp_thms, fresh_thms) = ListPair.unzip (map ListPair.unzip
(map (fn ((((i, (_, _, constrs)), tname), inject_thms'), perm_thms') =>
let val T = nth_dtyp' i
- in List.concat (map (fn (cname, dts) => map (fn atom =>
+ in maps (fn (cname, dts) => map (fn atom =>
let
val cname = Sign.intern_const thy8
(Long_Name.append tname (Long_Name.base_name cname));
@@ -1028,7 +1026,7 @@
else foldr1 HOLogic.mk_conj (map fresh args2)))))
(fn _ =>
simp_tac (HOL_ss addsimps [Un_iff, empty_iff, fresh_def, supp_thm]) 1))
- end) atoms) constrs)
+ end) atoms) constrs
end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ inject_thms ~~ perm_simps')));
(**** weak induction theorem ****)
@@ -1103,7 +1101,7 @@
ALLGOALS (asm_full_simp_tac (global_simpset_of thy8 addsimps
(abs_supp @ supp_atm @
PureThy.get_thms thy8 ("fs_" ^ Long_Name.base_name atom ^ "1") @
- List.concat supp_thms))))),
+ flat supp_thms))))),
length new_type_names))
end) atoms;
@@ -1156,9 +1154,9 @@
mk_fresh1 (y :: xs) ys;
fun mk_fresh2 xss [] = []
- | mk_fresh2 xss ((p as (ys, _)) :: yss) = List.concat (map (fn y as (_, T) =>
+ | mk_fresh2 xss ((p as (ys, _)) :: yss) = maps (fn y as (_, T) =>
map (fn (_, x as (_, U)) => HOLogic.mk_Trueprop
- (fresh_const T U $ Free y $ Free x)) (rev xss @ yss)) ys) @
+ (fresh_const T U $ Free y $ Free x)) (rev xss @ yss)) ys @
mk_fresh2 (p :: xss) yss;
fun make_ind_prem fsT f k T ((cname, cargs), idxs) =
@@ -1182,8 +1180,8 @@
val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs');
val prems' = map (fn p as (_, T) => HOLogic.mk_Trueprop
- (f T (Free p) (Free z))) (List.concat (map fst frees')) @
- mk_fresh1 [] (List.concat (map fst frees')) @
+ (f T (Free p) (Free z))) (maps fst frees') @
+ mk_fresh1 [] (maps fst frees') @
mk_fresh2 [] frees'
in list_all_free (frees @ [z], Logic.list_implies (prems' @ prems,
@@ -1191,10 +1189,10 @@
list_comb (Const (cname, Ts ---> T), map Free frees))))
end;
- val ind_prems = List.concat (map (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
+ val ind_prems = maps (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
map (make_ind_prem fsT (fn T => fn t => fn u =>
fresh_const T fsT $ t $ u) i T)
- (constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs));
+ (constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs);
val tnames = DatatypeProp.make_tnames recTs;
val zs = Name.variant_list tnames (replicate (length descr'') "z");
val ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
@@ -1208,10 +1206,10 @@
HOLogic.mk_Trueprop (Const ("Finite_Set.finite",
(snd (split_last (binder_types T)) --> HOLogic.boolT) -->
HOLogic.boolT) $ (f $ Free ("x", fsT'))))) fresh_fs @
- List.concat (map (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
+ maps (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
map (make_ind_prem fsT' (fn T => fn t => fn u => HOLogic.Not $
HOLogic.mk_mem (t, the (AList.lookup op = fresh_fs T) $ u)) i T)
- (constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs));
+ (constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs);
val ind_concl' = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
(map (fn ((((i, _), T), tname), z) =>
make_pred fsT' i T $ Free (z, fsT') $ Free (tname, T))
@@ -1448,10 +1446,10 @@
Free (a, T --> HOLogic.boolT)) (pnames ~~ rec_result_Ts);
fun mk_fresh3 rs [] = []
- | mk_fresh3 rs ((p as (ys, z)) :: yss) = List.concat (map (fn y as (_, T) =>
- List.mapPartial (fn ((_, (_, x)), r as (_, U)) => if z = x then NONE
+ | mk_fresh3 rs ((p as (ys, z)) :: yss) = maps (fn y as (_, T) =>
+ map_filter (fn ((_, (_, x)), r as (_, U)) => if z = x then NONE
else SOME (HOLogic.mk_Trueprop
- (fresh_const T U $ Free y $ Free r))) rs) ys) @
+ (fresh_const T U $ Free y $ Free r))) rs) ys @
mk_fresh3 rs yss;
(* FIXME: avoid collisions with other variable names? *)
@@ -1463,9 +1461,9 @@
val Ts = map (typ_of_dtyp descr'' sorts) cargs;
val frees = map (fn i => "x" ^ string_of_int i) (1 upto length Ts) ~~ Ts;
val frees' = partition_cargs idxs frees;
- val binders = List.concat (map fst frees');
+ val binders = maps fst frees';
val atomTs = distinct op = (maps (map snd o fst) frees');
- val recs = List.mapPartial
+ val recs = map_filter
(fn ((_, DtRec i), p) => SOME (i, p) | _ => NONE)
(partition_cargs idxs cargs ~~ frees');
val frees'' = map (fn i => "y" ^ string_of_int i) (1 upto length recs) ~~
@@ -1490,14 +1488,14 @@
fresh_const T (fastype_of result) $ Free p $ result) binders;
val P = HOLogic.mk_Trueprop (p $ result)
in
- (rec_intr_ts @ [Logic.list_implies (List.concat prems2 @ prems3 @ prems1,
+ (rec_intr_ts @ [Logic.list_implies (flat prems2 @ prems3 @ prems1,
HOLogic.mk_Trueprop (rec_set $
list_comb (Const (cname, Ts ---> T), map Free frees) $ result))],
rec_prems @ [list_all_free (frees @ frees'', Logic.list_implies (prems4, P))],
rec_prems' @ map (fn fr => list_all_free (frees @ frees'',
Logic.list_implies (List.nth (prems2, l) @ prems3 @ prems5 @ prems7 @ prems6 @ [P],
HOLogic.mk_Trueprop fr))) result_freshs,
- rec_eq_prems @ [List.concat prems2 @ prems3],
+ rec_eq_prems @ [flat prems2 @ prems3],
l + 1)
end;
@@ -1709,7 +1707,7 @@
val rec_unique_thms = split_conj_thm (Goal.prove
(ProofContext.init thy11) (map fst rec_unique_frees)
(map (augment_sort thy11 fs_cp_sort)
- (List.concat finite_premss @ finite_ctxt_prems @ rec_prems @ rec_prems'))
+ (flat finite_premss @ finite_ctxt_prems @ rec_prems @ rec_prems'))
(augment_sort thy11 fs_cp_sort
(HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj rec_unique_concls)))
(fn {prems, context} =>
@@ -1747,7 +1745,7 @@
(resolve_tac rec_intrs THEN_ALL_NEW atac) 1,
rotate_tac ~1 1,
((DETERM o etac elim) THEN_ALL_NEW full_simp_tac
- (HOL_ss addsimps List.concat distinct_thms)) 1] @
+ (HOL_ss addsimps flat distinct_thms)) 1] @
(if null idxs then [] else [hyp_subst_tac 1,
SUBPROOF (fn {asms, concl, prems = prems', params, context = context', ...} =>
let
@@ -1758,10 +1756,10 @@
val rT = fastype_of lhs';
val (c, cargsl) = strip_comb lhs;
val cargsl' = partition_cargs idxs cargsl;
- val boundsl = List.concat (map fst cargsl');
+ val boundsl = maps fst cargsl';
val (_, cargsr) = strip_comb rhs;
val cargsr' = partition_cargs idxs cargsr;
- val boundsr = List.concat (map fst cargsr');
+ val boundsr = maps fst cargsr';
val (params1, _ :: params2) =
chop (length params div 2) (map (term_of o #2) params);
val params' = params1 @ params2;
@@ -1779,8 +1777,7 @@
val _ = warning "step 1: obtaining fresh names";
val (freshs1, freshs2, context'') = fold
(obtain_fresh_name (rec_ctxt :: rec_fns' @ params')
- (List.concat (map snd finite_thss) @
- finite_ctxt_ths @ rec_prems)
+ (maps snd finite_thss @ finite_ctxt_ths @ rec_prems)
rec_fin_supp_thms')
Ts ([], [], context');
val pi1 = map perm_of_pair (boundsl ~~ freshs1);
@@ -1794,7 +1791,7 @@
(** as, bs, cs # K as ts, K bs us **)
val _ = warning "step 2: as, bs, cs # K as ts, K bs us";
val prove_fresh_ss = HOL_ss addsimps
- (finite_Diff :: List.concat fresh_thms @
+ (finite_Diff :: flat fresh_thms @
fs_atoms @ abs_fresh @ abs_supp @ fresh_atm);
(* FIXME: avoid asm_full_simp_tac ? *)
fun prove_fresh ths y x = Goal.prove context'' [] []
@@ -1826,9 +1823,9 @@
(fn _ => EVERY
[cut_facts_tac [pi1_pi2_eq] 1,
asm_full_simp_tac (HOL_ss addsimps
- (calc_atm @ List.concat perm_simps' @
+ (calc_atm @ flat perm_simps' @
fresh_prems' @ freshs2' @ abs_perm @
- alpha @ List.concat inject_thms)) 1]))
+ alpha @ flat inject_thms)) 1]))
(map snd cargsl' ~~ map snd cargsr');
(** pi1^-1 o pi2 o us = ts **)
@@ -1896,13 +1893,13 @@
(** as # rs **)
val _ = warning "step 8: as # rs";
- val rec_freshs = List.concat
- (map (fn (rec_prem, ih) =>
+ val rec_freshs =
+ maps (fn (rec_prem, ih) =>
let
val _ $ (S $ x $ (y as Free (_, T))) =
prop_of rec_prem;
val k = find_index (equal S) rec_sets;
- val atoms = List.concat (List.mapPartial (fn (bs, z) =>
+ val atoms = flat (map_filter (fn (bs, z) =>
if z = x then NONE else SOME bs) cargsl')
in
map (fn a as Free (_, aT) =>
@@ -1917,7 +1914,7 @@
[rtac rec_prem 1, rtac ih 1,
REPEAT_DETERM (resolve_tac fresh_prems 1)]))
end) atoms
- end) (rec_prems1 ~~ ihs));
+ end) (rec_prems1 ~~ ihs);
(** as # fK as ts rs , bs # fK bs us vs **)
val _ = warning "step 9: as # fK as ts rs , bs # fK bs us vs";
@@ -1969,7 +1966,7 @@
NominalPermeq.fresh_guess_tac
(HOL_ss addsimps (freshs2 @
fs_atoms @ fresh_atm @
- List.concat (map snd finite_thss))) 1]);
+ maps snd finite_thss)) 1]);
val fresh_results' =
map (prove_fresh_result' rec_prems1 rhs') freshs1 @
@@ -2031,7 +2028,7 @@
val ps = map (fn (x as Free (_, T), i) =>
(Free ("x" ^ string_of_int i, T), x)) (cargs ~~ (1 upto length cargs));
val concl' = subst_atomic_types (rec_result_Ts' ~~ rec_result_Ts) concl;
- val prems' = List.concat finite_premss @ finite_ctxt_prems @
+ val prems' = flat finite_premss @ finite_ctxt_prems @
rec_prems @ rec_prems' @ map (subst_atomic ps) prems;
fun solve rules prems = resolve_tac rules THEN_ALL_NEW
(resolve_tac prems THEN_ALL_NEW atac)
@@ -2054,10 +2051,10 @@
(* FIXME: theorems are stored in database for testing only *)
val (_, thy13) = thy12 |>
PureThy.add_thmss
- [((Binding.name "rec_equiv", List.concat rec_equiv_thms), []),
- ((Binding.name "rec_equiv'", List.concat rec_equiv_thms'), []),
- ((Binding.name "rec_fin_supp", List.concat rec_fin_supp_thms), []),
- ((Binding.name "rec_fresh", List.concat rec_fresh_thms), []),
+ [((Binding.name "rec_equiv", flat rec_equiv_thms), []),
+ ((Binding.name "rec_equiv'", flat rec_equiv_thms'), []),
+ ((Binding.name "rec_fin_supp", flat rec_fin_supp_thms), []),
+ ((Binding.name "rec_fresh", flat rec_fresh_thms), []),
((Binding.name "rec_unique", map standard rec_unique_thms), []),
((Binding.name "recs", rec_thms), [])] ||>
Sign.parent_path ||>
--- a/src/HOL/Nominal/nominal_induct.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Nominal/nominal_induct.ML Thu Oct 15 23:28:10 2009 +0200
@@ -50,10 +50,10 @@
in
(P, tuple_fun (map #2 avoiding) (Term.dest_Var P)) ::
(x, tuple (map Free avoiding)) ::
- List.mapPartial (fn (z, SOME t) => SOME (z, t) | _ => NONE) (zs ~~ inst)
+ map_filter (fn (z, SOME t) => SOME (z, t) | _ => NONE) (zs ~~ inst)
end;
val substs =
- map2 subst insts concls |> List.concat |> distinct (op =)
+ map2 subst insts concls |> flat |> distinct (op =)
|> map (pairself (Thm.cterm_of (ProofContext.theory_of ctxt)));
in
(((cases, nconcls), consumes), Drule.cterm_instantiate substs joined_rule)
@@ -98,7 +98,7 @@
(fn i => fn st =>
rules
|> inst_mutual_rule ctxt insts avoiding
- |> RuleCases.consume (List.concat defs) facts
+ |> 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/HOL/Nominal/nominal_inductive.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Thu Oct 15 23:28:10 2009 +0200
@@ -224,7 +224,7 @@
| lift_prem t = t;
fun mk_distinct [] = []
- | mk_distinct ((x, T) :: xs) = List.mapPartial (fn (y, U) =>
+ | mk_distinct ((x, T) :: xs) = map_filter (fn (y, U) =>
if T = U then SOME (HOLogic.mk_Trueprop
(HOLogic.mk_not (HOLogic.eq_const T $ x $ y)))
else NONE) xs @ mk_distinct xs;
@@ -263,7 +263,7 @@
val vc_compat = map (fn (params, bvars, prems, (p, ts)) =>
map (fn q => list_all (params, incr_boundvars ~1 (Logic.list_implies
- (List.mapPartial (fn prem =>
+ (map_filter (fn prem =>
if null (preds_of ps prem) then SOME prem
else map_term (split_conj (K o I) names) prem prem) prems, q))))
(mk_distinct bvars @
@@ -359,7 +359,7 @@
(etac conjunct1 1) monos NONE th,
mk_pi (the (map_thm ctxt (inst_conj_all names ps (rev pis''))
(inst_conj_all_tac (length pis'')) monos (SOME t) th))))
- (gprems ~~ oprems)) |>> List.mapPartial I;
+ (gprems ~~ oprems)) |>> map_filter I;
val vc_compat_ths' = map (fn th =>
let
val th' = first_order_mrs gprems1 th;
--- a/src/HOL/Nominal/nominal_inductive2.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Thu Oct 15 23:28:10 2009 +0200
@@ -279,7 +279,7 @@
val (vc_compat, vc_compat') = map (fn (params, sets, prems, (p, ts)) =>
map (fn q => abs_params params (incr_boundvars ~1 (Logic.list_implies
- (List.mapPartial (fn prem =>
+ (map_filter (fn prem =>
if null (preds_of ps prem) then SOME prem
else map_term (split_conj (K o I) names) prem prem) prems, q))))
(maps (fn (t, T) => map (fn (u, U) => HOLogic.mk_Trueprop
@@ -366,7 +366,7 @@
val pi_sets = map (fn (t, _) =>
fold_rev (NominalDatatype.mk_perm []) pis t) sets';
val (P, ts) = strip_comb (HOLogic.dest_Trueprop (term_of concl));
- val gprems1 = List.mapPartial (fn (th, t) =>
+ val gprems1 = map_filter (fn (th, t) =>
if null (preds_of ps t) then SOME th
else
map_thm ctxt' (split_conj (K o I) names)
--- a/src/HOL/Product_Type.thy Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Product_Type.thy Thu Oct 15 23:28:10 2009 +0200
@@ -1017,7 +1017,7 @@
(Codegen.invoke_codegen thy defs dep thyname true) ts gr2
in
SOME (Codegen.mk_app brack
- (Pretty.blk (0, [Codegen.str "let ", Pretty.blk (0, List.concat
+ (Pretty.blk (0, [Codegen.str "let ", Pretty.blk (0, flat
(separate [Codegen.str ";", Pretty.brk 1] (map (fn (pl, pr) =>
[Pretty.block [Codegen.str "val ", pl, Codegen.str " =",
Pretty.brk 1, pr]]) qs))),
--- a/src/HOL/Prolog/prolog.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Prolog/prolog.ML Thu Oct 15 23:28:10 2009 +0200
@@ -106,7 +106,7 @@
in Library.foldl (op APPEND) (no_tac, ptacs) st end;
fun ptac ctxt prog = let
- val proga = List.concat (map (atomizeD ctxt) prog) (* atomize the prog *)
+ val proga = maps (atomizeD ctxt) prog (* atomize the prog *)
in (REPEAT_DETERM1 o FIRST' [
rtac TrueI, (* "True" *)
rtac conjI, (* "[| P; Q |] ==> P & Q" *)
--- a/src/HOL/Statespace/state_fun.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Statespace/state_fun.ML Thu Oct 15 23:28:10 2009 +0200
@@ -333,7 +333,7 @@
[] => ""
| c::cs => String.implode (Char.toUpper c::cs ))
-fun mkName (Type (T,args)) = concat (map mkName args) ^ mkUpper (Long_Name.base_name T)
+fun mkName (Type (T,args)) = implode (map mkName args) ^ mkUpper (Long_Name.base_name T)
| mkName (TFree (x,_)) = mkUpper (Long_Name.base_name x)
| mkName (TVar ((x,_),_)) = mkUpper (Long_Name.base_name x);
@@ -347,7 +347,7 @@
| gen_constr_destr comp prfx thy (T as Type ("fun",_)) =
let val (argTs,rangeT) = strip_type T;
in comp
- (Syntax.const (deco prfx (concat (map mkName argTs) ^ "Fun")))
+ (Syntax.const (deco prfx (implode (map mkName argTs) ^ "Fun")))
(fold (fn x => fn y => x$y)
(replicate (length argTs) (Syntax.const "StateFun.map_fun"))
(gen_constr_destr comp prfx thy rangeT))
@@ -361,7 +361,7 @@
((mk_map T $ gen_constr_destr comp prfx thy argT))
| _ => raise (TYPE ("StateFun.gen_constr_destr",[T'],[])))
else (* type args are not recursively embedded into val *)
- Syntax.const (deco prfx (concat (map mkName argTs) ^ mkUpper (Long_Name.base_name T)))
+ Syntax.const (deco prfx (implode (map mkName argTs) ^ mkUpper (Long_Name.base_name T)))
| gen_constr_destr thy _ _ T = raise (TYPE ("StateFun.gen_constr_destr",[T],[]));
val mk_constr = gen_constr_destr (fn a => fn b => Syntax.const "Fun.comp" $ a $ b) ""
--- a/src/HOL/Statespace/state_space.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Statespace/state_space.ML Thu Oct 15 23:28:10 2009 +0200
@@ -369,7 +369,7 @@
val inst = map fst args ~~ Ts;
val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst);
val parent_comps =
- List.concat (map (fn (Ts',n,rs) => parent_components thy (map subst Ts',n,rs)) parents);
+ maps (fn (Ts',n,rs) => parent_components thy (map subst Ts',n,rs)) parents;
val all_comps = rename renaming (parent_comps @ map (apsnd subst) components);
in all_comps end;
@@ -403,10 +403,9 @@
(("",false),Expression.Positional
[SOME (Free (project_name T,projectT T)),
SOME (Free ((inject_name T,injectT T)))]))) Ts;
- val locs = flat (map (fn T => [(Binding.name (project_name T),NONE,NoSyn),
- (Binding.name (inject_name T),NONE,NoSyn)]) Ts);
- val constrains = List.concat
- (map (fn T => [(project_name T,projectT T),(inject_name T,injectT T)]) Ts);
+ val locs = maps (fn T => [(Binding.name (project_name T),NONE,NoSyn),
+ (Binding.name (inject_name T),NONE,NoSyn)]) Ts;
+ val constrains = maps (fn T => [(project_name T,projectT T),(inject_name T,injectT T)]) Ts;
fun interprete_parent_valuetypes (Ts, pname, _) thy =
let
@@ -414,7 +413,7 @@
the (Symtab.lookup (StateSpaceData.get (Context.Theory thy)) pname);
val inst = map fst args ~~ Ts;
val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst);
- val pars = List.concat (map ((fn T => [project_name T,inject_name T]) o subst) types);
+ val pars = maps ((fn T => [project_name T,inject_name T]) o subst) types;
val expr = ([(suffix valuetypesN name,
(("",false),Expression.Positional (map SOME pars)))],[]);
@@ -562,7 +561,7 @@
fun fst_eq ((x:string,_),(y,_)) = x = y;
fun snd_eq ((_,t:typ),(_,u)) = t = u;
- val raw_parent_comps = (List.concat (map (parent_components thy) parents'));
+ val raw_parent_comps = maps (parent_components thy) parents';
fun check_type (n,T) =
(case distinct (snd_eq) (filter (curry fst_eq (n,T)) raw_parent_comps) of
[] => []
@@ -570,7 +569,7 @@
| rs => ["Different types for component " ^ n ^": " ^
commas (map (Syntax.string_of_typ ctxt o snd) rs)])
- val err_dup_types = List.concat (map check_type (duplicates fst_eq raw_parent_comps))
+ val err_dup_types = maps check_type (duplicates fst_eq raw_parent_comps)
val parent_comps = distinct (fst_eq) raw_parent_comps;
val all_comps = parent_comps @ comps';
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Thu Oct 15 23:28:10 2009 +0200
@@ -49,7 +49,7 @@
let
val _ = message config "Proving case distinction theorems ...";
- val descr' = List.concat descr;
+ val descr' = flat descr;
val recTs = get_rec_types descr' sorts;
val newTs = Library.take (length (hd descr), recTs);
@@ -95,7 +95,7 @@
val big_name = space_implode "_" new_type_names;
val thy0 = Sign.add_path big_name thy;
- val descr' = List.concat descr;
+ val descr' = flat descr;
val recTs = get_rec_types descr' sorts;
val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
val newTs = Library.take (length (hd descr), recTs);
@@ -278,7 +278,7 @@
val thy1 = Sign.add_path (space_implode "_" new_type_names) thy;
- val descr' = List.concat descr;
+ val descr' = flat descr;
val recTs = get_rec_types descr' sorts;
val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
val newTs = Library.take (length (hd descr), recTs);
@@ -312,14 +312,14 @@
end) (constrs ~~ (1 upto length constrs)));
val caseT = (map (snd o dest_Free) fns1) @ [T] ---> T';
- val fns = (List.concat (Library.take (i, case_dummy_fns))) @
- fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns)));
+ val fns = flat (Library.take (i, case_dummy_fns)) @
+ fns2 @ flat (Library.drop (i + 1, case_dummy_fns));
val reccomb = Const (recname, (map fastype_of fns) @ [T] ---> T');
val decl = ((Binding.name (Long_Name.base_name name), caseT), NoSyn);
val def = (Binding.name (Long_Name.base_name name ^ "_def"),
Logic.mk_equals (list_comb (Const (name, caseT), fns1),
- list_comb (reccomb, (List.concat (Library.take (i, case_dummy_fns))) @
- fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns))) )));
+ list_comb (reccomb, (flat (Library.take (i, case_dummy_fns))) @
+ fns2 @ (flat (Library.drop (i + 1, case_dummy_fns))) )));
val ([def_thm], thy') =
thy
|> Sign.declare_const [] decl |> snd
--- a/src/HOL/Tools/Datatype/datatype_aux.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML Thu Oct 15 23:28:10 2009 +0200
@@ -124,7 +124,7 @@
| _ => NONE)
| SOME (_ $ t') => SOME (Abs ("x", fastype_of t', abstract_over (t', t2))))
val cert = cterm_of (Thm.theory_of_thm st);
- val insts = List.mapPartial (fn (t, u) => case abstr (getP u) of
+ val insts = map_filter (fn (t, u) => case abstr (getP u) of
NONE => NONE
| SOME u' => SOME (t |> getP |> snd |> head_of |> cert, cert u')) (ts ~~ ts');
val indrule' = cterm_instantiate insts indrule
@@ -279,7 +279,7 @@
fun check_nonempty descr =
let
- val descr' = List.concat descr;
+ val descr' = flat descr;
fun is_nonempty_dt is i =
let
val (_, _, constrs) = (the o AList.lookup (op =) descr') i;
--- a/src/HOL/Tools/Datatype/datatype_case.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_case.ML Thu Oct 15 23:28:10 2009 +0200
@@ -241,8 +241,7 @@
val types = map type_of (case_functions @ [u]);
val case_const = Const (case_name, types ---> range_ty)
val tree = list_comb (case_const, case_functions @ [u])
- val pat_rect1 = flat (map mk_pat
- (constructors ~~ constructors' ~~ pat_rect))
+ val pat_rect1 = maps mk_pat (constructors ~~ constructors' ~~ pat_rect)
in (pat_rect1, tree)
end)
| SOME (t, i) => raise CASE_ERROR ("Not a datatype constructor: " ^
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Thu Oct 15 23:28:10 2009 +0200
@@ -69,17 +69,17 @@
(if null tvs then [] else
[mk_tuple (map str tvs), str " "]) @
[str (type_id ^ " ="), Pretty.brk 1] @
- List.concat (separate [Pretty.brk 1, str "| "]
+ flat (separate [Pretty.brk 1, str "| "]
(map (fn (ps', (_, cname)) => [Pretty.block
(str cname ::
(if null ps' then [] else
- List.concat ([str " of", Pretty.brk 1] ::
+ flat ([str " of", Pretty.brk 1] ::
separate [str " *", Pretty.brk 1]
(map single ps'))))]) ps))) :: rest, gr''')
end;
fun mk_constr_term cname Ts T ps =
- List.concat (separate [str " $", Pretty.brk 1]
+ flat (separate [str " $", Pretty.brk 1]
([str ("Const (\"" ^ cname ^ "\","), Pretty.brk 1,
mk_type false (Ts ---> T), str ")"] :: ps));
@@ -148,7 +148,7 @@
fun mk_choice [c] = mk_constr "(i-1)" false c
| mk_choice cs = Pretty.block [str "one_of",
Pretty.brk 1, Pretty.blk (1, str "[" ::
- List.concat (separate [str ",", Pretty.fbrk]
+ flat (separate [str ",", Pretty.fbrk]
(map (single o mk_delay o mk_constr "(i-1)" false) cs)) @
[str "]"]), Pretty.brk 1, str "()"];
@@ -242,7 +242,7 @@
end;
val (ps1, gr1) = pcase constrs ts1 Ts gr ;
- val ps = List.concat (separate [Pretty.brk 1, str "| "] ps1);
+ val ps = flat (separate [Pretty.brk 1, str "| "] ps1);
val (p, gr2) = invoke_codegen thy defs dep module false t gr1;
val (ps2, gr3) = fold_map (invoke_codegen thy defs dep module true) ts2 gr2;
in ((if not (null ts2) andalso brack then parens else I)
--- a/src/HOL/Tools/Datatype/datatype_prop.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML Thu Oct 15 23:28:10 2009 +0200
@@ -113,7 +113,7 @@
fun make_ind descr sorts =
let
- val descr' = List.concat descr;
+ val descr' = flat descr;
val recTs = get_rec_types descr' sorts;
val pnames = if length descr' = 1 then ["P"]
else map (fn i => "P" ^ string_of_int i) (1 upto length descr');
@@ -143,8 +143,8 @@
list_comb (Const (cname, Ts ---> T), map Free frees))))
end;
- val prems = List.concat (map (fn ((i, (_, _, constrs)), T) =>
- map (make_ind_prem i T) constrs) (descr' ~~ recTs));
+ val prems = maps (fn ((i, (_, _, constrs)), T) =>
+ map (make_ind_prem i T) constrs) (descr' ~~ recTs);
val tnames = make_tnames recTs;
val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
(map (fn (((i, _), T), tname) => make_pred i T $ Free (tname, T))
@@ -156,7 +156,7 @@
fun make_casedists descr sorts =
let
- val descr' = List.concat descr;
+ val descr' = flat descr;
fun make_casedist_prem T (cname, cargs) =
let
@@ -181,12 +181,12 @@
fun make_primrec_Ts descr sorts used =
let
- val descr' = List.concat descr;
+ val descr' = flat descr;
val rec_result_Ts = map TFree (Name.variant_list used (replicate (length descr') "'t") ~~
replicate (length descr') HOLogic.typeS);
- val reccomb_fn_Ts = List.concat (map (fn (i, (_, _, constrs)) =>
+ val reccomb_fn_Ts = maps (fn (i, (_, _, constrs)) =>
map (fn (_, cargs) =>
let
val Ts = map (typ_of_dtyp descr' sorts) cargs;
@@ -197,13 +197,13 @@
val argTs = Ts @ map mk_argT recs
in argTs ---> List.nth (rec_result_Ts, i)
- end) constrs) descr');
+ end) constrs) descr';
in (rec_result_Ts, reccomb_fn_Ts) end;
fun make_primrecs new_type_names descr sorts thy =
let
- val descr' = List.concat descr;
+ val descr' = flat descr;
val recTs = get_rec_types descr' sorts;
val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
@@ -253,7 +253,7 @@
fun make_case_combs new_type_names descr sorts thy fname =
let
- val descr' = List.concat descr;
+ val descr' = flat descr;
val recTs = get_rec_types descr' sorts;
val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
val newTs = Library.take (length (hd descr), recTs);
@@ -277,7 +277,7 @@
fun make_cases new_type_names descr sorts thy =
let
- val descr' = List.concat descr;
+ val descr' = flat descr;
val recTs = get_rec_types descr' sorts;
val newTs = Library.take (length (hd descr), recTs);
@@ -300,7 +300,7 @@
fun make_splits new_type_names descr sorts thy =
let
- val descr' = List.concat descr;
+ val descr' = flat descr;
val recTs = get_rec_types descr' sorts;
val used' = List.foldr OldTerm.add_typ_tfree_names [] recTs;
val newTs = Library.take (length (hd descr), recTs);
@@ -412,7 +412,7 @@
fun make_nchotomys descr sorts =
let
- val descr' = List.concat descr;
+ val descr' = flat descr;
val recTs = get_rec_types descr' sorts;
val newTs = Library.take (length (hd descr), recTs);
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Thu Oct 15 23:28:10 2009 +0200
@@ -103,7 +103,7 @@
(list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Bound 0) (Bound 0)))
(descr ~~ recTs ~~ rec_result_Ts ~~ rec_names);
val r = if null is then Extraction.nullt else
- foldr1 HOLogic.mk_prod (List.mapPartial (fn (((((i, _), T), U), s), tname) =>
+ foldr1 HOLogic.mk_prod (map_filter (fn (((((i, _), T), U), s), tname) =>
if i mem is then SOME
(list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Free (tname, T))
else NONE) (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names ~~ tnames));
--- a/src/HOL/Tools/Function/fundef.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Tools/Function/fundef.ML Thu Oct 15 23:28:10 2009 +0200
@@ -58,7 +58,7 @@
val (saved_spec_simps, lthy) =
fold_map (LocalTheory.note Thm.generatedK) spec lthy
- val saved_simps = flat (map snd saved_spec_simps)
+ val saved_simps = maps snd saved_spec_simps
val simps_by_f = sort saved_simps
fun add_for_f fname simps =
--- a/src/HOL/Tools/Function/lexicographic_order.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Thu Oct 15 23:28:10 2009 +0200
@@ -137,7 +137,7 @@
(** Error reporting **)
-fun pr_table table = writeln (cat_lines (map (fn r => concat (map pr_cell r)) table))
+fun pr_table table = writeln (cat_lines (map (fn r => implode (map pr_cell r)) table))
fun pr_goals ctxt st =
Goal_Display.pretty_goals ctxt {total = true, main = false, maxgoals = Thm.nprems_of st} st
@@ -176,8 +176,8 @@
val gc = map (fn i => chr (i + 96)) (1 upto length table)
val mc = 1 upto length measure_funs
- val tstr = "Result matrix:" :: (" " ^ concat (map (enclose " " " " o string_of_int) mc))
- :: map2 (fn r => fn i => i ^ ": " ^ concat (map pr_cell r)) table gc
+ val tstr = "Result matrix:" :: (" " ^ implode (map (enclose " " " " o string_of_int) mc))
+ :: map2 (fn r => fn i => i ^ ": " ^ implode (map pr_cell r)) table gc
val gstr = "Calls:" :: map2 (prefix " " oo pr_goal) tl gc
val mstr = "Measures:" :: map2 (prefix " " oo pr_fun) measure_funs mc
val ustr = "Unfinished subgoals:" :: pr_unprovable_subgoals ctxt table
--- a/src/HOL/Tools/Function/pattern_split.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Tools/Function/pattern_split.ML Thu Oct 15 23:28:10 2009 +0200
@@ -70,7 +70,7 @@
map (fn (vs, subst) => (vs, (v,t)::subst)) substs
end
in
- flat (map foo (inst_constrs_of (ProofContext.theory_of ctx) T))
+ maps foo (inst_constrs_of (ProofContext.theory_of ctx) T)
end
| pattern_subtract_subst_aux vs t t' =
let
@@ -110,7 +110,7 @@
(* ps - p' *)
fun pattern_subtract_from_many ctx p'=
- flat o map (pattern_subtract ctx p')
+ maps (pattern_subtract ctx p')
(* in reverse order *)
fun pattern_subtract_many ctx ps' =
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Thu Oct 15 23:28:10 2009 +0200
@@ -316,7 +316,7 @@
fun index xs = (1 upto length xs) ~~ xs
fun outp s t f xs = map (fn (x, y) => s ^ Int.toString x ^ t ^ f y ^ "\n") xs
val ims = index (map index ms)
- val _ = tracing (concat (outp "fn #" ":\n" (concat o outp "\tmeasure #" ": " (Syntax.string_of_term ctxt)) ims))
+ val _ = tracing (implode (outp "fn #" ":\n" (implode o outp "\tmeasure #" ": " (Syntax.string_of_term ctxt)) ims))
fun print_call (k, c) =
let
val (_, p, _, q, _, _) = dest_call D c
@@ -325,8 +325,8 @@
val caller_ms = nth ms p
val callee_ms = nth ms q
val entries = map (fn x => map (pair x) (callee_ms)) (caller_ms)
- fun print_ln (i : int, l) = concat (Int.toString i :: " " :: map (enclose " " " " o print_cell o (uncurry (get_descent D c))) l)
- val _ = tracing (concat (Int.toString (p + 1) ^ "|" ^ Int.toString (q + 1) ^
+ fun print_ln (i : int, l) = implode (Int.toString i :: " " :: map (enclose " " " " o print_cell o (uncurry (get_descent D c))) l)
+ val _ = tracing (implode (Int.toString (p + 1) ^ "|" ^ Int.toString (q + 1) ^
" " :: map (enclose " " " " o Int.toString) (1 upto length callee_ms)) ^ "\n"
^ cat_lines (map print_ln ((1 upto (length entries)) ~~ entries)))
in
--- a/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML Thu Oct 15 23:28:10 2009 +0200
@@ -42,7 +42,7 @@
(case DatatypePackage.get_datatype thy ((fst o dest_Type o fastype_of) t) of
NONE => false
| SOME info => (let
- val constr_consts = flat (map (fn (_, (_, _, constrs)) => map fst constrs) (#descr info))
+ val constr_consts = maps (fn (_, (_, _, constrs)) => map fst constrs) (#descr info)
val (c, _) = strip_comb t
in (case c of
Const (name, _) => name mem_string constr_consts
@@ -183,7 +183,7 @@
String.isSuffix "_case" (List.last splitted_name)
then
(List.take (splitted_name, length splitted_name - 1)) @ ["split"]
- |> String.concatWith "."
+ |> space_implode "."
|> PureThy.get_thm thy
|> SOME
handle ERROR msg => NONE
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Oct 15 23:28:10 2009 +0200
@@ -982,7 +982,7 @@
val (out_ts', in_ts') = List.partition (is_constrt thy) out_ts;
val vTs = maps term_vTs out_ts';
val dupTs = map snd (duplicates (op =) vTs) @
- List.mapPartial (AList.lookup (op =) vTs) vs;
+ map_filter (AList.lookup (op =) vTs) vs;
in
terms_vs (in_ts @ in_ts') subset vs andalso
forall (is_eqT o fastype_of) in_ts' andalso
@@ -1033,10 +1033,10 @@
val _ = tracing ("iss:" ^
commas (map (fn is => case is of SOME is => string_of_smode is | NONE => "NONE") iss))
*)
- val modes' = modes @ List.mapPartial
+ val modes' = modes @ map_filter
(fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
(param_vs ~~ iss);
- val gen_modes' = gen_modes @ List.mapPartial
+ val gen_modes' = gen_modes @ map_filter
(fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
(param_vs ~~ iss);
val vTs = distinct (op =) ((fold o fold_prem) Term.add_frees ps (fold Term.add_frees ts []))
@@ -1783,9 +1783,9 @@
if (is_constructor thy t) then let
val case_rewrites = (#case_rewrites (Datatype.the_info thy
((fst o dest_Type o fastype_of) t)))
- in case_rewrites @ (flat (map get_case_rewrite (snd (strip_comb t)))) end
+ in case_rewrites @ maps get_case_rewrite (snd (strip_comb t)) end
else []
- val simprules = @{thm "unit.cases"} :: @{thm "prod.cases"} :: (flat (map get_case_rewrite out_ts))
+ val simprules = @{thm "unit.cases"} :: @{thm "prod.cases"} :: maps get_case_rewrite out_ts
(* replace TRY by determining if it necessary - are there equations when calling compile match? *)
in
(* make this simpset better! *)
--- a/src/HOL/Tools/TFL/casesplit.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Tools/TFL/casesplit.ML Thu Oct 15 23:28:10 2009 +0200
@@ -305,7 +305,7 @@
fun derive_init_eqs sgn rules eqs =
let
fun get_related_thms i =
- List.mapPartial ((fn (r, x) => if x = i then SOME r else NONE));
+ map_filter ((fn (r, x) => if x = i then SOME r else NONE));
fun add_eq (i, e) xs =
(e, (get_related_thms i rules), i) :: xs
fun solve_eq (th, [], i) =
--- a/src/HOL/Tools/TFL/post.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Tools/TFL/post.ML Thu Oct 15 23:28:10 2009 +0200
@@ -188,7 +188,7 @@
-- Lucas Dixon, Aug 2004 *)
local
fun get_related_thms i =
- List.mapPartial ((fn (r,x) => if x = i then SOME r else NONE));
+ map_filter ((fn (r,x) => if x = i then SOME r else NONE));
fun solve_eq (th, [], i) =
error "derive_init_eqs: missing rules"
@@ -209,8 +209,7 @@
fun countlist l =
(rev o snd o (Library.foldl (fn ((i,L), e) => (i + 1,(e,i) :: L)))) ((0,[]), l)
in
- List.concat (map (fn (e,i) => solve_eq (e, (get_related_thms i rules), i))
- (countlist eqths))
+ maps (fn (e,i) => solve_eq (e, (get_related_thms i rules), i)) (countlist eqths)
end;
end;
--- a/src/HOL/Tools/TFL/tfl.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML Thu Oct 15 23:28:10 2009 +0200
@@ -258,7 +258,7 @@
| SOME{case_const,constructors} =>
let
val case_const_name = #1(dest_Const case_const)
- val nrows = List.concat (map (expand constructors pty) rows)
+ val nrows = maps (expand constructors pty) rows
val subproblems = divide(constructors, pty, range_ty, nrows)
val groups = map #group subproblems
and new_formals = map #new_formals subproblems
@@ -272,8 +272,7 @@
val types = map type_of (case_functions@[u]) @ [range_ty]
val case_const' = Const(case_const_name, list_mk_type types)
val tree = list_comb(case_const', case_functions@[u])
- val pat_rect1 = List.concat
- (ListPair.map mk_pat (constructors', pat_rect))
+ val pat_rect1 = flat (ListPair.map mk_pat (constructors', pat_rect))
in (pat_rect1,tree)
end
end end
--- a/src/HOL/Tools/TFL/thry.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Tools/TFL/thry.ML Thu Oct 15 23:28:10 2009 +0200
@@ -73,9 +73,9 @@
constructors = (map Const o the o Datatype.get_constrs thy) dtco};
fun extract_info thy =
- let val infos = (map snd o Symtab.dest o Datatype.get_all) thy
+ let val infos = map snd (Symtab.dest (Datatype.get_all thy))
in {case_congs = map (mk_meta_eq o #case_cong) infos,
- case_rewrites = List.concat (map (map mk_meta_eq o #case_rewrites) infos)}
+ case_rewrites = maps (map mk_meta_eq o #case_rewrites) infos}
end;
--- a/src/HOL/Tools/inductive.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Tools/inductive.ML Thu Oct 15 23:28:10 2009 +0200
@@ -329,7 +329,7 @@
REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI'}] 1),
REPEAT (FIRST
[atac 1,
- resolve_tac (List.concat (map mk_mono monos) @ get_monos ctxt) 1,
+ resolve_tac (maps mk_mono monos @ get_monos ctxt) 1,
etac @{thm le_funE} 1, dtac @{thm le_boolD} 1])]));
--- a/src/HOL/Tools/inductive_codegen.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Thu Oct 15 23:28:10 2009 +0200
@@ -129,7 +129,7 @@
string_of_mode ms)) modes));
val term_vs = map (fst o fst o dest_Var) o OldTerm.term_vars;
-val terms_vs = distinct (op =) o List.concat o (map term_vs);
+val terms_vs = distinct (op =) o maps term_vs;
(** collect all Vars in a term (with duplicates!) **)
fun term_vTs tm =
@@ -160,8 +160,8 @@
let
val ks = 1 upto length (binder_types (fastype_of t));
val default = [Mode (([], ks), ks, [])];
- fun mk_modes name args = Option.map (List.concat o
- map (fn (m as (iss, is)) =>
+ fun mk_modes name args = Option.map
+ (maps (fn (m as (iss, is)) =>
let
val (args1, args2) =
if length args < length iss then
@@ -198,9 +198,9 @@
let
val (in_ts, out_ts) = get_args is 1 us;
val (out_ts', in_ts') = List.partition (is_constrt thy) out_ts;
- val vTs = List.concat (map term_vTs out_ts');
+ val vTs = maps term_vTs out_ts';
val dupTs = map snd (duplicates (op =) vTs) @
- List.mapPartial (AList.lookup (op =) vTs) vs;
+ map_filter (AList.lookup (op =) vTs) vs;
in
terms_vs (in_ts @ in_ts') subset vs andalso
forall (is_eqT o fastype_of) in_ts' andalso
@@ -215,7 +215,7 @@
fun check_mode_clause thy arg_vs modes (iss, is) (ts, ps) =
let
- val modes' = modes @ List.mapPartial
+ val modes' = modes @ map_filter
(fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
(arg_vs ~~ iss);
fun check_mode_prems vs [] = SOME vs
@@ -228,7 +228,7 @@
val in_vs = terms_vs in_ts;
val concl_vs = terms_vs ts
in
- forall is_eqT (map snd (duplicates (op =) (List.concat (map term_vTs in_ts)))) andalso
+ forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso
forall (is_eqT o fastype_of) in_ts' andalso
(case check_mode_prems (arg_vs union in_vs) ps of
NONE => false
@@ -263,7 +263,7 @@
in mk_eqs x xs end;
fun mk_tuple xs = Pretty.block (str "(" ::
- List.concat (separate [str ",", Pretty.brk 1] (map single xs)) @
+ flat (separate [str ",", Pretty.brk 1] (map single xs)) @
[str ")"]);
fun mk_v ((names, vs), s) = (case AList.lookup (op =) vs s of
@@ -286,8 +286,8 @@
| is_exhaustive _ = false;
fun compile_match nvs eq_ps out_ps success_p can_fail =
- let val eqs = List.concat (separate [str " andalso", Pretty.brk 1]
- (map single (List.concat (map (mk_eq o snd) nvs) @ eq_ps)));
+ let val eqs = flat (separate [str " andalso", Pretty.brk 1]
+ (map single (maps (mk_eq o snd) nvs @ eq_ps)));
in
Pretty.block
([str "(fn ", mk_tuple out_ps, str " =>", Pretty.brk 1] @
@@ -305,7 +305,7 @@
else mk_const_id module s gr
in (space_implode "__"
(mk_qual_id module id ::
- map (space_implode "_" o map string_of_int) (List.mapPartial I iss @ [is])), gr')
+ map (space_implode "_" o map string_of_int) (map_filter I iss @ [is])), gr')
end;
fun mk_funcomp brack s k p = (if brack then parens else I)
@@ -332,7 +332,7 @@
(invoke_codegen thy defs dep module true) args2 gr')
in ((if brack andalso not (null ps andalso null ps') then
single o parens o Pretty.block else I)
- (List.concat (separate [Pretty.brk 1]
+ (flat (separate [Pretty.brk 1]
([str mode_id] :: ps @ map single ps'))), gr')
end
else apfst (single o mk_funcomp brack "??" (length (binder_types (fastype_of t))))
@@ -342,7 +342,7 @@
fun compile_clause thy defs dep module all_vs arg_vs modes (iss, is) (ts, ps) inp gr =
let
- val modes' = modes @ List.mapPartial
+ val modes' = modes @ map_filter
(fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
(arg_vs ~~ iss);
@@ -449,7 +449,7 @@
(case mode of ([], []) => [str "()"] | _ => xs)) @
[str " ="]),
Pretty.brk 1] @
- List.concat (separate [str " ++", Pretty.brk 1] (map single cl_ps))), (gr', "and "))
+ flat (separate [str " ++", Pretty.brk 1] (map single cl_ps))), (gr', "and "))
end;
fun compile_preds thy defs dep module all_vs arg_vs modes preds gr =
@@ -458,7 +458,7 @@
dep module prfx' all_vs arg_vs modes s cls mode gr')
(((the o AList.lookup (op =) modes) s))) preds (gr, "fun ")
in
- (space_implode "\n\n" (map string_of (List.concat prs)) ^ ";\n\n", gr')
+ (space_implode "\n\n" (map string_of (flat prs)) ^ ";\n\n", gr')
end;
(**** processing of introduction rules ****)
@@ -467,7 +467,7 @@
(string * (int list option list * int list) list) list *
(string * (int option list * int)) list;
-fun lookup_modes gr dep = apfst List.concat (apsnd List.concat (ListPair.unzip
+fun lookup_modes gr dep = apfst flat (apsnd flat (ListPair.unzip
(map ((fn (SOME (Modes x), _, _) => x | _ => ([], [])) o get_node gr)
(Graph.all_preds (fst gr) [dep]))));
@@ -502,7 +502,7 @@
let
val _ $ u = Logic.strip_imp_concl (hd intrs);
val args = List.take (snd (strip_comb u), nparms);
- val arg_vs = List.concat (map term_vs args);
+ val arg_vs = maps term_vs args;
fun get_nparms s = if s mem names then SOME nparms else
Option.map #3 (get_clauses thy s);
--- a/src/HOL/Tools/inductive_realizer.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Thu Oct 15 23:28:10 2009 +0200
@@ -225,7 +225,7 @@
let
val Type ("fun", [U, _]) = T;
val a :: names' = names
- in (list_abs_free (("x", U) :: List.mapPartial (fn intr =>
+ in (list_abs_free (("x", U) :: map_filter (fn intr =>
Option.map (pair (name_of_fn intr))
(AList.lookup (op =) frees (name_of_fn intr))) intrs,
list_comb (Const (a, Ts ---> T), fs) $ Free ("x", U)), names')
@@ -300,7 +300,7 @@
fold (fn s => AxClass.axiomatize_arity
(s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |>
Extraction.add_typeof_eqns_i ty_eqs;
- val dts = List.mapPartial (fn (s, rs) => if s mem rsets then
+ val dts = map_filter (fn (s, rs) => if s mem rsets then
SOME (dt_of_intrs thy1' vs nparms rs) else NONE) rss;
(** datatype representing computational content of inductive set **)
@@ -332,7 +332,7 @@
(Extraction.realizes_of thy2 vs
(if c = Extraction.nullt then c else list_comb (c, map Var (rev
(Term.add_vars (prop_of intr) []) \\ params'))) (prop_of intr)))
- (maps snd rss ~~ List.concat constrss);
+ (maps snd rss ~~ flat constrss);
val (rlzpreds, rlzpreds') =
rintrs |> map (fn rintr =>
let
@@ -470,9 +470,8 @@
(map (mk_realizer thy4 vs) (map (fn (((rule, rrule), rlz), c) =>
(name_of_thm rule, rule, rrule, rlz,
list_comb (c, map Var (rev (Term.add_vars (prop_of rule) []) \\ params'))))
- (List.concat (map snd rss) ~~ #intrs ind_info ~~ rintrs ~~
- List.concat constrss))) thy4;
- val elimps = List.mapPartial (fn ((s, intrs), p) =>
+ (maps snd rss ~~ #intrs ind_info ~~ rintrs ~~ flat constrss))) thy4;
+ val elimps = map_filter (fn ((s, intrs), p) =>
if s mem rsets then SOME (p, intrs) else NONE)
(rss' ~~ (elims ~~ #elims ind_info));
val thy6 = Library.foldl (fn (thy, p as (((((elim, _), _), _), _), _)) => thy |>
--- a/src/HOL/Tools/metis_tools.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Tools/metis_tools.ML Thu Oct 15 23:28:10 2009 +0200
@@ -384,8 +384,8 @@
SOME _ => NONE (*type instantiations are forbidden!*)
| NONE => SOME (a,t) (*internal Metis var?*)
val _ = Output.debug (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th)
- val substs = List.mapPartial remove_typeinst (Metis.Subst.toList fsubst)
- val (vars,rawtms) = ListPair.unzip (List.mapPartial subst_translation substs)
+ val substs = map_filter remove_typeinst (Metis.Subst.toList fsubst)
+ val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
val tms = infer_types ctxt rawtms;
val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
val substs' = ListPair.zip (vars, map ctm_of tms)
@@ -664,7 +664,7 @@
fun FOL_SOLVE mode ctxt cls ths0 =
let val thy = ProofContext.theory_of ctxt
val th_cls_pairs = map (fn th => (Thm.get_name_hint th, ResAxioms.cnf_axiom thy th)) ths0
- val ths = List.concat (map #2 th_cls_pairs)
+ val ths = maps #2 th_cls_pairs
val _ = Output.debug (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
val _ = app (fn th => Output.debug (fn () => Display.string_of_thm ctxt th)) cls
val _ = Output.debug (fn () => "THEOREM CLAUSES")
@@ -690,7 +690,7 @@
(*add constraints arising from converting goal to clause form*)
val proof = Metis.Proof.proof mth
val result = translate mode ctxt' axioms proof
- and used = List.mapPartial (used_axioms axioms) proof
+ and used = map_filter (used_axioms axioms) proof
val _ = Output.debug (fn () => "METIS COMPLETED...clauses actually used:")
val _ = app (fn th => Output.debug (fn () => Display.string_of_thm ctxt th)) used
val unused = filter (fn (a,cls) => not (common_thm used cls)) th_cls_pairs
--- a/src/HOL/Tools/recdef.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Tools/recdef.ML Thu Oct 15 23:28:10 2009 +0200
@@ -209,7 +209,7 @@
thy
|> Sign.add_path bname
|> PureThy.add_thmss
- (((Binding.name "simps", List.concat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
+ (((Binding.name "simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
||>> PureThy.add_thms [((Binding.name "induct", induct), [])];
val result = {simps = simps', rules = rules', induct = induct', tcs = tcs};
val thy =
--- a/src/HOL/Tools/recfun_codegen.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML Thu Oct 15 23:28:10 2009 +0200
@@ -119,7 +119,7 @@
let
val thmss as (_, thyname) :: _ = map (get_equations thy defs) cs;
val module' = if_library thyname module;
- val eqs'' = map (dest_eq o prop_of) (List.concat (map fst thmss));
+ val eqs'' = map (dest_eq o prop_of) (maps fst thmss);
val (fundef', gr3) = mk_fundef module' "" true eqs''
(add_edge (dname, dep)
(List.foldr (uncurry new_node) (del_nodes xs gr2)
--- a/src/HOL/Tools/record.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Tools/record.ML Thu Oct 15 23:28:10 2009 +0200
@@ -656,7 +656,7 @@
fun bad_inst ((x, S), T) =
if Sign.of_sort thy (T, S) then NONE else SOME x
- val bads = List.mapPartial bad_inst (args ~~ types);
+ val bads = map_filter bad_inst (args ~~ types);
val _ = null bads orelse err ("Ill-sorted instantiation of " ^ commas bads ^ " in");
val inst = map fst args ~~ types;
@@ -1362,7 +1362,7 @@
| mk_updterm us _ _ = raise TERM ("mk_updterm match", map (fn (x, _, _) => x) us);
val (lhs, rhs, vars, _, simp, noops) = mk_updterm upds Symtab.empty base;
- val noops' = flat (map snd (Symtab.dest noops));
+ val noops' = maps snd (Symtab.dest noops);
in
if simp then
SOME
@@ -1521,7 +1521,7 @@
end)
| split_free_tac _ _ _ = NONE;
- val split_frees_tacs = List.mapPartial (split_free_tac P i) frees;
+ val split_frees_tacs = map_filter (split_free_tac P i) frees;
val simprocs = if has_rec goal then [record_split_simproc P] else [];
val thms' = K_comp_convs @ thms;
@@ -1860,7 +1860,7 @@
val (bfields, field_syntax) =
split_list (map (fn (x, T, mx) => ((x, T), mx)) raw_fields);
- val parent_fields = List.concat (map #fields parents);
+ val parent_fields = maps #fields parents;
val parent_chunks = map (length o #fields) parents;
val parent_names = map fst parent_fields;
val parent_types = map snd parent_fields;
--- a/src/HOL/Tools/refute.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Tools/refute.ML Thu Oct 15 23:28:10 2009 +0200
@@ -281,7 +281,7 @@
if null terms then
"empty interpretation (no free variables in term)\n"
else
- cat_lines (List.mapPartial (fn (t, intr) =>
+ cat_lines (map_filter (fn (t, intr) =>
(* print constants only if 'show_consts' is true *)
if (!show_consts) orelse not (is_Const t) then
SOME (Syntax.string_of_term_global thy t ^ ": " ^
@@ -395,7 +395,7 @@
(* TODO: it is currently not possible to specify a size for a type *)
(* whose name is one of the other parameters (e.g. 'maxvars') *)
(* (string * int) list *)
- val sizes = List.mapPartial
+ val sizes = map_filter
(fn (name, value) => Option.map (pair name) (Int.fromString value))
(List.filter (fn (name, _) => name<>"minsize" andalso name<>"maxsize"
andalso name<>"maxvars" andalso name<>"maxtime"
@@ -994,8 +994,7 @@
(* collect argument types *)
val acc_dtyps = List.foldr collect_dtyp acc_dT dtyps
(* collect constructor types *)
- val acc_dconstrs = List.foldr collect_dtyp acc_dtyps
- (List.concat (map snd dconstrs))
+ val acc_dconstrs = List.foldr collect_dtyp acc_dtyps (maps snd dconstrs)
in
acc_dconstrs
end
@@ -1389,7 +1388,7 @@
map single xs
| pick_all n xs =
let val rec_pick = pick_all (n-1) xs in
- List.concat (map (fn x => map (cons x) rec_pick) xs)
+ maps (fn x => map (cons x) rec_pick) xs
end
(* returns all constant interpretations that have the same tree *)
(* structure as the interpretation argument *)
@@ -1582,7 +1581,7 @@
map single xs
| pick_all (xs::xss) =
let val rec_pick = pick_all xss in
- List.concat (map (fn x => map (cons x) rec_pick) xs)
+ maps (fn x => map (cons x) rec_pick) xs
end
| pick_all _ =
raise REFUTE ("interpretation_apply", "empty list (in pick_all)")
@@ -2068,7 +2067,7 @@
map single xs
| pick_all n xs =
let val rec_pick = pick_all (n-1) xs in
- List.concat (map (fn x => map (cons x) rec_pick) xs)
+ maps (fn x => map (cons x) rec_pick) xs
end
(* ["x1", ..., "xn"] *)
val terms1 = canonical_terms typs T1
@@ -2131,13 +2130,13 @@
end
in
(* C_i ... < C_j ... if i < j *)
- List.concat (map (fn (cname, ctyps) =>
+ maps (fn (cname, ctyps) =>
let
val cTerm = Const (cname,
map (typ_of_dtyp descr typ_assoc) ctyps ---> T)
in
constructor_terms [cTerm] ctyps
- end) constrs)
+ end) constrs
end)
| NONE =>
(* not an inductive datatype; in this case the argument types in *)
@@ -2483,14 +2482,14 @@
(* of the parameter must be ignored *)
if List.exists (equal True) xs then [pi] else []
| ci_pi (Node xs, Node ys) =
- List.concat (map ci_pi (xs ~~ ys))
+ maps ci_pi (xs ~~ ys)
| ci_pi (Node _, Leaf _) =
raise REFUTE ("IDT_recursion_interpreter",
"constructor takes more arguments than the " ^
"associated parameter")
(* (int * interpretation list) list *)
val rec_operators = map (fn (idx, c_p_intrs) =>
- (idx, List.concat (map ci_pi c_p_intrs))) mc_p_intrs
+ (idx, maps ci_pi c_p_intrs)) mc_p_intrs
(* sanity check: every recursion operator must provide as *)
(* many values as the corresponding datatype *)
(* has elements *)
@@ -3080,8 +3079,7 @@
val constants_T = make_constants thy model T
val size_U = size_of_type thy model U
in
- SOME (Node (List.concat (map (replicate size_U) constants_T)),
- model, args)
+ SOME (Node (maps (replicate size_U) constants_T), model, args)
end
| _ =>
NONE;
@@ -3100,7 +3098,7 @@
val size_T = size_of_type thy model T
val constants_U = make_constants thy model U
in
- SOME (Node (List.concat (replicate size_T constants_U)), model, args)
+ SOME (Node (flat (replicate size_T constants_U)), model, args)
end
| _ =>
NONE;
--- a/src/HOL/Tools/res_atp.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Tools/res_atp.ML Thu Oct 15 23:28:10 2009 +0200
@@ -251,7 +251,7 @@
let fun relevant ([],_) [] = [] : (thm * (string * int)) list (*Nothing added this iteration*)
| relevant (newpairs,rejects) [] =
let val (newrels,more_rejects) = take_best max_new newpairs
- val new_consts = List.concat (map #2 newrels)
+ val new_consts = maps #2 newrels
val rel_consts' = List.foldl add_const_typ_table rel_consts new_consts
val newp = p + (1.0-p) / convergence
in
@@ -425,7 +425,7 @@
(* Type Classes Present in the Axiom or Conjecture Clauses *)
(***************************************************************)
-fun add_classes (sorts, cset) = List.foldl setinsert cset (List.concat sorts);
+fun add_classes (sorts, cset) = List.foldl setinsert cset (flat sorts);
(*Remove this trivial type class*)
fun delete_type cset = Symtab.delete_safe "HOL.type" cset;
--- a/src/HOL/Tools/res_reconstruct.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML Thu Oct 15 23:28:10 2009 +0200
@@ -422,7 +422,7 @@
fun fix lno = if lno <= Vector.length thm_names
then SOME(Vector.sub(thm_names,lno-1))
else AList.lookup op= deps_map lno;
- in (lname, t, List.mapPartial fix (distinct (op=) deps)) ::
+ in (lname, t, map_filter fix (distinct (op=) deps)) ::
stringify_deps thm_names ((lno,lname)::deps_map) lines
end;
@@ -451,7 +451,7 @@
val ilines = isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines)
val _ = trace "\ndecode_tstp_file: finishing\n"
in
- isar_header (map #1 fixes) ^ String.concat ilines ^ "qed\n"
+ isar_header (map #1 fixes) ^ implode ilines ^ "qed\n"
end;
@@ -504,7 +504,7 @@
| inputno ("cnf"::ntok::"negated"::"conjecture"::_) = Int.fromString ntok
| inputno _ = NONE
val lines = split_lines proofextract
- in List.mapPartial (inputno o toks) lines end
+ in map_filter (inputno o toks) lines end
(*String contains multiple lines. We want those of the form
"253[0:Inp] et cetera..."
A list consisting of the first number in each line is returned. *)
@@ -513,7 +513,7 @@
fun inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok
| inputno _ = NONE
val lines = split_lines proofextract
- in List.mapPartial (inputno o toks) lines end
+ in map_filter (inputno o toks) lines end
(*extracting lemmas from tstp-output between the lines from above*)
fun extract_lemmas get_step_nums (proof, thm_names, conj_count, _, _, _) =
--- a/src/HOL/Tools/sat_solver.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/Tools/sat_solver.ML Thu Oct 15 23:28:10 2009 +0200
@@ -233,7 +233,7 @@
let
(* string -> int list *)
fun int_list_from_string s =
- List.mapPartial Int.fromString (space_explode " " s)
+ map_filter Int.fromString (space_explode " " s)
(* int list -> assignment *)
fun assignment_from_list [] i =
NONE (* the SAT solver didn't provide a value for this variable *)
@@ -350,8 +350,7 @@
o (map (map literal_from_int))
o clauses
o (map int_from_string)
- o List.concat
- o (map (String.fields (fn c => c mem [#" ", #"\t", #"\n"])))
+ o (maps (String.fields (fn c => c mem [#" ", #"\t", #"\n"])))
o filter_preamble
o (List.filter (fn l => l <> ""))
o split_lines
--- a/src/HOL/ex/predicate_compile.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML Thu Oct 15 23:28:10 2009 +0200
@@ -906,7 +906,7 @@
val (out_ts', in_ts') = List.partition (is_constrt thy) out_ts;
val vTs = maps term_vTs out_ts';
val dupTs = map snd (duplicates (op =) vTs) @
- List.mapPartial (AList.lookup (op =) vTs) vs;
+ map_filter (AList.lookup (op =) vTs) vs;
in
terms_vs (in_ts @ in_ts') subset vs andalso
forall (is_eqT o fastype_of) in_ts' andalso
@@ -950,10 +950,10 @@
fun check_mode_clause with_generator thy param_vs modes gen_modes (iss, is) (ts, ps) =
let
- val modes' = modes @ List.mapPartial
+ val modes' = modes @ map_filter
(fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
(param_vs ~~ iss);
- val gen_modes' = gen_modes @ List.mapPartial
+ val gen_modes' = gen_modes @ map_filter
(fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
(param_vs ~~ iss);
val vTs = distinct (op =) ((fold o fold_prem) Term.add_frees ps (fold Term.add_frees ts []))
@@ -1547,9 +1547,9 @@
if (is_constructor thy t) then let
val case_rewrites = (#case_rewrites (Datatype.the_info thy
((fst o dest_Type o fastype_of) t)))
- in case_rewrites @ (flat (map get_case_rewrite (snd (strip_comb t)))) end
+ in case_rewrites @ maps get_case_rewrite (snd (strip_comb t)) end
else []
- val simprules = @{thm "unit.cases"} :: @{thm "prod.cases"} :: (flat (map get_case_rewrite out_ts))
+ val simprules = @{thm "unit.cases"} :: @{thm "prod.cases"} :: maps get_case_rewrite out_ts
(* replace TRY by determining if it necessary - are there equations when calling compile match? *)
in
(* make this simpset better! *)
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Thu Oct 15 23:28:10 2009 +0200
@@ -123,7 +123,7 @@
list_ccomb(%%:(dname^"_when"),map
(fn (con',args) => if con'<>con then UU else
List.foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg);
- in List.mapPartial I (List.concat(map (fn (con,args) => mapn (sdef con) 1 args) cons)) end;
+ in map_filter I (maps (fn (con,args) => mapn (sdef con) 1 args) cons) end;
(* ----- axiom and definitions concerning induction ------------------------- *)
--- a/src/HOLCF/Tools/Domain/domain_extender.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML Thu Oct 15 23:28:10 2009 +0200
@@ -33,12 +33,12 @@
val test_dupl_typs = (case duplicates (op =) (map fst dtnvs) of
[] => false | dups => error ("Duplicate types: " ^ commas_quote dups));
val test_dupl_cons =
- (case duplicates (op =) (map (Binding.name_of o first) (List.concat cons'')) of
+ (case duplicates (op =) (map (Binding.name_of o first) (flat cons'')) of
[] => false | dups => error ("Duplicate constructors: "
^ commas_quote dups));
val test_dupl_sels =
- (case duplicates (op =) (map Binding.name_of (List.mapPartial second
- (List.concat (map second (List.concat cons''))))) of
+ (case duplicates (op =) (map Binding.name_of (map_filter second
+ (maps second (flat cons'')))) of
[] => false | dups => error("Duplicate selectors: "^commas_quote dups));
val test_dupl_tvars =
exists(fn s=>case duplicates (op =) (map(fst o dest_TFree)s)of
@@ -142,7 +142,7 @@
in
theorems_thy
|> Sign.add_path (Long_Name.base_name comp_dnam)
- |> (snd o (PureThy.add_thmss [((Binding.name "rews", List.concat rewss @ take_rews), [])]))
+ |> (snd o (PureThy.add_thmss [((Binding.name "rews", flat rewss @ take_rews), [])]))
|> Sign.parent_path
end;
--- a/src/HOLCF/Tools/Domain/domain_syntax.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOLCF/Tools/Domain/domain_syntax.ML Thu Oct 15 23:28:10 2009 +0200
@@ -76,7 +76,7 @@
mk_matT(dtype, map third args, freetvar "t" 1),
Mixfix(escape ("match_" ^ Binding.name_of con), [], Syntax.max_pri));
fun sel1 (_,sel,typ) = Option.map (fn s => (s,dtype ->> typ,NoSyn)) sel;
- fun sel (con,args,mx) = List.mapPartial sel1 args;
+ fun sel (con,args,mx) = map_filter sel1 args;
fun mk_patT (a,b) = a ->> mk_maybeT b;
fun pat_arg_typ n arg = mk_patT (third arg, freetvar "t" n);
fun pat (con,args,mx) = (pat_name_ con,
@@ -90,7 +90,7 @@
val consts_dis = map dis cons';
val consts_mat = map mat cons';
val consts_pat = map pat cons';
- val consts_sel = List.concat(map sel cons');
+ val consts_sel = maps sel cons';
end;
(* ----- constants concerning induction ------------------------------------- *)
@@ -147,7 +147,7 @@
PrintRule (Library.foldl capp (cname, ListPair.map (app "_match") (ps,vs)),
app "_match" (mk_appl pname ps, args_list vs))]
end;
- val Case_trans = List.concat (map one_case_trans cons');
+ val Case_trans = maps one_case_trans cons';
end;
end;
@@ -172,10 +172,10 @@
val const_copy = (Binding.name (comp_dnam^"_copy"), funprod ->> funprod, NoSyn);
val const_bisim = (Binding.name (comp_dnam^"_bisim"), relprod --> boolT, NoSyn);
val ctt : ((binding * typ * mixfix) list * ast Syntax.trrule list) list = map (calc_syntax funprod) eqs';
- in thy'' |> ContConsts.add_consts_i (List.concat (map fst ctt) @
+ in thy'' |> ContConsts.add_consts_i (maps fst ctt @
(if length eqs'>1 then [const_copy] else[])@
[const_bisim])
- |> Sign.add_trrules_i (List.concat(map snd ctt))
+ |> Sign.add_trrules_i (maps snd ctt)
end; (* let *)
end; (* struct *)
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Thu Oct 15 23:28:10 2009 +0200
@@ -149,7 +149,7 @@
let
fun def_of_sel sel = ga (sel^"_def") dname;
fun def_of_arg arg = Option.map def_of_sel (sel_of arg);
- fun defs_of_con (_, args) = List.mapPartial def_of_arg args;
+ fun defs_of_con (_, args) = map_filter def_of_arg args;
in
maps defs_of_con cons
end;
@@ -434,7 +434,7 @@
(K [simp_tac (HOLCF_ss addsimps when_rews) 1]);
fun sel_strict (_, args) =
- List.mapPartial (Option.map one_sel o sel_of) args;
+ map_filter (Option.map one_sel o sel_of) args;
in
val _ = trace " Proving sel_stricts...";
val sel_stricts = maps sel_strict cons;
@@ -492,7 +492,7 @@
val _ = trace " Proving sel_defins...";
val sel_defins =
if length cons = 1
- then List.mapPartial (fn arg => Option.map sel_defin (sel_of arg))
+ then map_filter (fn arg => Option.map sel_defin (sel_of arg))
(filter_out is_lazy (snd (hd cons)))
else [];
end;
--- a/src/HOLCF/Tools/fixrec.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/HOLCF/Tools/fixrec.ML Thu Oct 15 23:28:10 2009 +0200
@@ -371,7 +371,7 @@
val simps1 : (Attrib.binding * thm list) list =
map (fn (n,xs) => (mk_bind n, map snd xs)) (names ~~ simps);
val simps2 : (Attrib.binding * thm list) list =
- map (apsnd (fn thm => [thm])) (List.concat simps);
+ map (apsnd (fn thm => [thm])) (flat simps);
val (_, lthy'') = lthy'
|> fold_map (LocalTheory.note Thm.generatedK) (simps1 @ simps2);
in
--- a/src/Provers/Arith/fast_lin_arith.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Thu Oct 15 23:28:10 2009 +0200
@@ -720,7 +720,7 @@
val mkleq = mklineq n atoms
val ixs = 0 upto (n - 1)
val iatoms = atoms ~~ ixs
- val natlineqs = List.mapPartial (mknat Ts ixs) iatoms
+ val natlineqs = map_filter (mknat Ts ixs) iatoms
val ineqs = map mkleq initems @ natlineqs
in case elim (ineqs, []) of
Success j =>
--- a/src/Provers/classical.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/Provers/classical.ML Thu Oct 15 23:28:10 2009 +0200
@@ -938,7 +938,7 @@
val ruleq = Drule.multi_resolves facts rules;
in
Method.trace ctxt rules;
- fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq)
+ fn st => Seq.maps (fn rule => Tactic.rtac rule i st) ruleq
end)
THEN_ALL_NEW Goal.norm_hhf_tac;
--- a/src/Provers/order.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/Provers/order.ML Thu Oct 15 23:28:10 2009 +0200
@@ -735,7 +735,7 @@
ListPair.map (fn (a,b) => (a,b)) (0 upto (length components -1), components);
fun indexNodes IndexComp =
- List.concat (map (fn (index, comp) => (map (fn v => (v,index)) comp)) IndexComp);
+ maps (fn (index, comp) => (map (fn v => (v,index)) comp)) IndexComp;
fun getIndex v [] = ~1
| getIndex v ((v',k)::vs) = if v aconv v' then k else getIndex v vs;
@@ -1142,9 +1142,9 @@
fun processComponent (k, comp) =
let
(* all edges with weight <= of the actual component *)
- val leqEdges = List.concat (map (adjacent (op aconv) leqG) comp);
+ val leqEdges = maps (adjacent (op aconv) leqG) comp;
(* all edges with weight ~= of the actual component *)
- val neqEdges = map snd (List.concat (map (adjacent (op aconv) neqG) comp));
+ val neqEdges = map snd (maps (adjacent (op aconv) neqG) comp);
(* find an edge leading to a contradiction *)
fun findContr [] = NONE
@@ -1231,7 +1231,7 @@
val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A));
val Hs = map prop_of prems @ map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
- val lesss = List.concat (ListPair.map (mkasm decomp less_thms thy) (Hs, 0 upto (length Hs - 1)))
+ val lesss = flat (ListPair.map (mkasm decomp less_thms thy) (Hs, 0 upto (length Hs - 1)))
val prfs = gen_solve mkconcl thy (lesss, C);
val (subgoals, prf) = mkconcl decomp less_thms thy C;
in
--- a/src/Provers/quasi.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/Provers/quasi.ML Thu Oct 15 23:28:10 2009 +0200
@@ -555,7 +555,7 @@
val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A));
val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A);
val C = subst_bounds (rfrees, Logic.strip_assums_concl A);
- val lesss = List.concat (ListPair.map (mkasm_trans thy) (Hs, 0 upto (length Hs - 1)));
+ val lesss = flat (ListPair.map (mkasm_trans thy) (Hs, 0 upto (length Hs - 1)));
val prfs = solveLeTrans thy (lesss, C);
val (subgoal, prf) = mkconcl_trans thy C;
--- a/src/Pure/codegen.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/Pure/codegen.ML Thu Oct 15 23:28:10 2009 +0200
@@ -742,8 +742,7 @@
fun mk_tuple [p] = p
| mk_tuple ps = Pretty.block (str "(" ::
- List.concat (separate [str ",", Pretty.brk 1] (map single ps)) @
- [str ")"]);
+ flat (separate [str ",", Pretty.brk 1] (map single ps)) @ [str ")"]);
fun mk_let bindings body =
Pretty.blk (0, [str "let", Pretty.brk 1,
--- a/src/Tools/Compute_Oracle/am_ghc.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/Tools/Compute_Oracle/am_ghc.ML Thu Oct 15 23:28:10 2009 +0200
@@ -84,7 +84,7 @@
in
if a <= len then
let
- val s = "c"^(str c)^(concat (map (fn t => " "^(protect_blank (print_term d t))) (List.take (args, a))))
+ val s = "c"^(str c)^(implode (map (fn t => " "^(protect_blank (print_term d t))) (List.take (args, a))))
in
print_apps d s (List.drop (args, a))
end
@@ -154,19 +154,19 @@
val rules = group_rules rules
val constants = Inttab.keys arity
fun arity_of c = Inttab.lookup arity c
- fun rep_str s n = concat (rep n s)
+ fun rep_str s n = implode (rep n s)
fun indexed s n = s^(str n)
fun section n = if n = 0 then [] else (section (n-1))@[n-1]
fun make_show c =
let
val args = section (the (arity_of c))
in
- " show ("^(indexed "C" c)^(concat (map (indexed " a") args))^") = "
- ^"\""^(indexed "C" c)^"\""^(concat (map (fn a => "++(show "^(indexed "a" a)^")") args))
+ " show ("^(indexed "C" c)^(implode (map (indexed " a") args))^") = "
+ ^"\""^(indexed "C" c)^"\""^(implode (map (fn a => "++(show "^(indexed "a" a)^")") args))
end
fun default_case c =
let
- val args = concat (map (indexed " x") (section (the (arity_of c))))
+ val args = implode (map (indexed " x") (section (the (arity_of c))))
in
(indexed "c" c)^args^" = "^(indexed "C" c)^args
end
@@ -174,7 +174,7 @@
"module "^name^" where",
"",
"data Term = Const Integer | App Term Term | Abs (Term -> Term)",
- " "^(concat (map (fn c => " | C"^(str c)^(rep_str " Term" (the (arity_of c)))) constants)),
+ " "^(implode (map (fn c => " | C"^(str c)^(rep_str " Term" (the (arity_of c)))) constants)),
"",
"instance Show Term where"]
val _ = writelist (map make_show constants)
--- a/src/Tools/Compute_Oracle/am_sml.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/Tools/Compute_Oracle/am_sml.ML Thu Oct 15 23:28:10 2009 +0200
@@ -206,8 +206,8 @@
let
val strict_a = (case toplevel_arity_of c of SOME sa => sa | NONE => a)
val _ = if strict_a > a then raise Compile "strict" else ()
- val s = module_prefix^"c"^(str c)^(concat (map (fn t => " "^(protect_blank (print_term d t))) (List.take (args, strict_a))))
- val s = s^(concat (map (fn t => " (fn () => "^print_term d t^")") (List.drop (List.take (args, a), strict_a))))
+ val s = module_prefix^"c"^(str c)^(implode (map (fn t => " "^(protect_blank (print_term d t))) (List.take (args, strict_a))))
+ val s = s^(implode (map (fn t => " (fn () => "^print_term d t^")") (List.drop (List.take (args, a), strict_a))))
in
print_apps d s (List.drop (args, a))
end
@@ -273,9 +273,9 @@
val lazy_vars = the (arity_of c) - the (toplevel_arity_of c)
fun print_tm tm = print_term NONE arity_of toplevel_arity_of n lazy_vars tm
fun print_guard (Guard (a,b)) = "term_eq ("^(print_tm a)^") ("^(print_tm b)^")"
- val else_branch = "c"^(str c)^"_"^(str (gnum+1))^(concat (map (fn i => " a"^(str i)) (section (the (arity_of c)))))
+ val else_branch = "c"^(str c)^"_"^(str (gnum+1))^(implode (map (fn i => " a"^(str i)) (section (the (arity_of c)))))
fun print_guards t [] = print_tm t
- | print_guards t (g::gs) = "if ("^(print_guard g)^")"^(concat (map (fn g => " andalso ("^(print_guard g)^")") gs))^" then ("^(print_tm t)^") else "^else_branch
+ | print_guards t (g::gs) = "if ("^(print_guard g)^")"^(implode (map (fn g => " andalso ("^(print_guard g)^")") gs))^" then ("^(print_tm t)^") else "^else_branch
in
(if null guards then gnum else gnum+1, pattern^" = "^(print_guards t guards))
end
@@ -307,15 +307,15 @@
val constants = Inttab.keys arity
fun arity_of c = Inttab.lookup arity c
fun toplevel_arity_of c = Inttab.lookup toplevel_arity c
- fun rep_str s n = concat (rep n s)
+ fun rep_str s n = implode (rep n s)
fun indexed s n = s^(str n)
fun string_of_tuple [] = ""
- | string_of_tuple (x::xs) = "("^x^(concat (map (fn s => ", "^s) xs))^")"
+ | string_of_tuple (x::xs) = "("^x^(implode (map (fn s => ", "^s) xs))^")"
fun string_of_args [] = ""
- | string_of_args (x::xs) = x^(concat (map (fn s => " "^s) xs))
+ | string_of_args (x::xs) = x^(implode (map (fn s => " "^s) xs))
fun default_case gnum c =
let
- val leftargs = concat (map (indexed " x") (section (the (arity_of c))))
+ val leftargs = implode (map (indexed " x") (section (the (arity_of c))))
val rightargs = section (the (arity_of c))
val strict_args = (case toplevel_arity_of c of NONE => the (arity_of c) | SOME sa => sa)
val xs = map (fn n => if n < strict_args then "x"^(str n) else "x"^(str n)^"()") rightargs
@@ -374,7 +374,7 @@
"structure "^name^" = struct",
"",
"datatype Term = Const of int | App of Term * Term | Abs of (Term -> Term)",
- " "^(concat (map (fn c => " | C"^(str c)^(mk_constr_type_args (the (arity_of c)))) constants)),
+ " "^(implode (map (fn c => " | C"^(str c)^(mk_constr_type_args (the (arity_of c)))) constants)),
""]
fun make_constr c argprefix = "(C"^(str c)^" "^(string_of_tuple (map (fn i => argprefix^(str i)) (section (the (arity_of c)))))^")"
fun make_term_eq c = " | term_eq "^(make_constr c "a")^" "^(make_constr c "b")^" = "^
@@ -385,7 +385,7 @@
val eqs = map (fn i => "term_eq a"^(str i)^" b"^(str i)) (section n)
val (eq, eqs) = (List.hd eqs, map (fn s => " andalso "^s) (List.tl eqs))
in
- eq^(concat eqs)
+ eq^(implode eqs)
end)
val _ = writelist [
"fun term_eq (Const c1) (Const c2) = (c1 = c2)",
@@ -421,7 +421,7 @@
(gnum, r::l)::rs
else
let
- val args = concat (map (fn i => " a"^(str i)) (section (the (arity_of c))))
+ val args = implode (map (fn i => " a"^(str i)) (section (the (arity_of c))))
fun gnumc g = if g > 0 then "c"^(str c)^"_"^(str g)^args else "c"^(str c)^args
val s = gnumc (gnum) ^ " = " ^ gnumc (gnum')
in
@@ -444,7 +444,7 @@
val leftargs =
case args of
[] => ""
- | (x::xs) => "("^x^(concat (map (fn s => ", "^s) xs))^")"
+ | (x::xs) => "("^x^(implode (map (fn s => ", "^s) xs))^")"
val args = map (indexed "convert a") (section (the (arity_of c)))
val right = fold (fn x => fn s => "AM_SML.App ("^s^", "^x^")") args ("AM_SML.Const "^(str c))
in
--- a/src/ZF/Tools/datatype_package.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/ZF/Tools/datatype_package.ML Thu Oct 15 23:28:10 2009 +0200
@@ -146,13 +146,13 @@
val (_, case_lists) = List.foldr add_case_list (1,[]) con_ty_lists;
(*extract the types of all the variables*)
- val case_typ = List.concat (map (map (#2 o #1)) con_ty_lists) ---> @{typ "i => i"};
+ val case_typ = maps (map (#2 o #1)) con_ty_lists ---> @{typ "i => i"};
val case_base_name = big_rec_base_name ^ "_case";
val case_name = full_name case_base_name;
(*The list of all the function variables*)
- val case_args = List.concat (map (map #1) case_lists);
+ val case_args = maps (map #1) case_lists;
val case_const = Const (case_name, case_typ);
val case_tm = list_comb (case_const, case_args);
@@ -218,19 +218,18 @@
val (_, recursor_lists) = List.foldr add_case_list (1,[]) rec_ty_lists;
(*extract the types of all the variables*)
- val recursor_typ = List.concat (map (map (#2 o #1)) rec_ty_lists) ---> @{typ "i => i"};
+ val recursor_typ = maps (map (#2 o #1)) rec_ty_lists ---> @{typ "i => i"};
val recursor_base_name = big_rec_base_name ^ "_rec";
val recursor_name = full_name recursor_base_name;
(*The list of all the function variables*)
- val recursor_args = List.concat (map (map #1) recursor_lists);
+ val recursor_args = maps (map #1) recursor_lists;
val recursor_tm =
list_comb (Const (recursor_name, recursor_typ), recursor_args);
- val recursor_cases = map call_recursor
- (List.concat case_lists ~~ List.concat recursor_lists)
+ val recursor_cases = map call_recursor (flat case_lists ~~ flat recursor_lists);
val recursor_def =
PrimitiveDefs.mk_defpair
@@ -252,16 +251,15 @@
val (con_defs, thy0) = thy_path
|> Sign.add_consts_i
(map (fn (c, T, mx) => (Binding.name c, T, mx))
- ((case_base_name, case_typ, NoSyn) :: map #1 (List.concat con_ty_lists)))
+ ((case_base_name, case_typ, NoSyn) :: map #1 (flat con_ty_lists)))
|> PureThy.add_defs false
(map (Thm.no_attributes o apfst Binding.name)
(case_def ::
- List.concat (ListPair.map mk_con_defs
- (1 upto npart, con_ty_lists))))
+ flat (ListPair.map mk_con_defs (1 upto npart, con_ty_lists))))
||> add_recursor
||> Sign.parent_path
- val intr_names = map (Binding.name o #2) (List.concat con_ty_lists);
+ val intr_names = map (Binding.name o #2) (flat con_ty_lists);
val (thy1, ind_result) =
thy0 |> Ind_Package.add_inductive_i
false (rec_tms, dom_sum) (map Thm.no_attributes (intr_names ~~ intr_tms))
@@ -296,9 +294,7 @@
val free_iffs = map standard (con_defs RL [@{thm def_swap_iff}]);
- val case_eqns =
- map prove_case_eqn
- (List.concat con_ty_lists ~~ case_args ~~ tl con_defs);
+ val case_eqns = map prove_case_eqn (flat con_ty_lists ~~ case_args ~~ tl con_defs);
(*** Prove the recursor theorems ***)
@@ -336,7 +332,7 @@
simp_tac (rank_ss addsimps case_eqns) 1,
IF_UNSOLVED (simp_tac (rank_ss addsimps tl con_defs) 1)]);
in
- map prove_recursor_eqn (List.concat con_ty_lists ~~ recursor_cases)
+ map prove_recursor_eqn (flat con_ty_lists ~~ recursor_cases)
end
val constructors =
--- a/src/ZF/Tools/induct_tacs.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/ZF/Tools/induct_tacs.ML Thu Oct 15 23:28:10 2009 +0200
@@ -74,7 +74,7 @@
let fun mk_pair (Const(@{const_name mem},_) $ Free (v,_) $ A) =
(v, #1 (dest_Const (head_of A)))
| mk_pair _ = raise Match
- val pairs = List.mapPartial (try (mk_pair o FOLogic.dest_Trueprop))
+ val pairs = map_filter (try (mk_pair o FOLogic.dest_Trueprop))
(#2 (OldGoals.strip_context Bi))
in case AList.lookup (op =) pairs var of
NONE => raise Find_tname ("Cannot determine datatype of " ^ quote var)
--- a/src/ZF/ind_syntax.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/ZF/ind_syntax.ML Thu Oct 15 23:28:10 2009 +0200
@@ -89,7 +89,7 @@
$ rec_tm))
in map mk_intr constructs end;
-fun mk_all_intr_tms sg arg = List.concat (ListPair.map (mk_intr_tms sg) arg);
+fun mk_all_intr_tms sg arg = flat (ListPair.map (mk_intr_tms sg) arg);
fun mk_Un (t1, t2) = @{const Un} $ t1 $ t2;
--- a/src/ZF/simpdata.ML Thu Oct 15 23:10:35 2009 +0200
+++ b/src/ZF/simpdata.ML Thu Oct 15 23:28:10 2009 +0200
@@ -16,9 +16,8 @@
case head_of t of
Const(a,_) =>
(case AList.lookup (op =) pairs a of
- SOME rls => List.concat (map (atomize (conn_pairs, mem_pairs))
- ([th] RL rls))
- | NONE => [th])
+ SOME rls => maps (atomize (conn_pairs, mem_pairs)) ([th] RL rls)
+ | NONE => [th])
| _ => [th]
in case concl_of th of
Const("Trueprop",_) $ P =>