replaced String.concat by implode;
authorwenzelm
Thu Oct 15 23:28:10 2009 +0200 (2009-10-15)
changeset 32952aeb1e44fbc19
parent 32951 83392f9d303f
child 32953 e52e6e5c0ca5
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;
src/FOL/simpdata.ML
src/FOLP/simp.ML
src/HOL/Import/xml.ML
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_induct.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Product_Type.thy
src/HOL/Prolog/prolog.ML
src/HOL/Statespace/state_fun.ML
src/HOL/Statespace/state_space.ML
src/HOL/Tools/Datatype/datatype_abs_proofs.ML
src/HOL/Tools/Datatype/datatype_aux.ML
src/HOL/Tools/Datatype/datatype_case.ML
src/HOL/Tools/Datatype/datatype_codegen.ML
src/HOL/Tools/Datatype/datatype_prop.ML
src/HOL/Tools/Datatype/datatype_realizer.ML
src/HOL/Tools/Function/fundef.ML
src/HOL/Tools/Function/lexicographic_order.ML
src/HOL/Tools/Function/pattern_split.ML
src/HOL/Tools/Function/scnp_reconstruct.ML
src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/TFL/casesplit.ML
src/HOL/Tools/TFL/post.ML
src/HOL/Tools/TFL/tfl.ML
src/HOL/Tools/TFL/thry.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/metis_tools.ML
src/HOL/Tools/recdef.ML
src/HOL/Tools/recfun_codegen.ML
src/HOL/Tools/record.ML
src/HOL/Tools/refute.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_reconstruct.ML
src/HOL/Tools/sat_solver.ML
src/HOL/ex/predicate_compile.ML
src/HOLCF/Tools/Domain/domain_axioms.ML
src/HOLCF/Tools/Domain/domain_extender.ML
src/HOLCF/Tools/Domain/domain_syntax.ML
src/HOLCF/Tools/Domain/domain_theorems.ML
src/HOLCF/Tools/fixrec.ML
src/Provers/Arith/fast_lin_arith.ML
src/Provers/classical.ML
src/Provers/order.ML
src/Provers/quasi.ML
src/Pure/codegen.ML
src/Tools/Compute_Oracle/am_ghc.ML
src/Tools/Compute_Oracle/am_sml.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/ind_syntax.ML
src/ZF/simpdata.ML
     1.1 --- a/src/FOL/simpdata.ML	Thu Oct 15 23:10:35 2009 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Thu Oct 15 23:28:10 2009 +0200
     1.3 @@ -46,7 +46,7 @@
     1.4               (case head_of p of
     1.5                  Const(a,_) =>
     1.6                    (case AList.lookup (op =) pairs a of
     1.7 -                     SOME(rls) => List.concat (map atoms ([th] RL rls))
     1.8 +                     SOME(rls) => maps atoms ([th] RL rls)
     1.9                     | NONE => [th])
    1.10                | _ => [th])
    1.11           | _ => [th])
     2.1 --- a/src/FOLP/simp.ML	Thu Oct 15 23:10:35 2009 +0200
     2.2 +++ b/src/FOLP/simp.ML	Thu Oct 15 23:28:10 2009 +0200
     2.3 @@ -432,8 +432,8 @@
     2.4  fun add_asms(ss,thm,a,anet,ats,cs) =
     2.5      let val As = strip_varify(nth_subgoal i thm, a, []);
     2.6          val thms = map (trivial o cterm_of(Thm.theory_of_thm thm)) As;
     2.7 -        val new_rws = List.concat(map mk_rew_rules thms);
     2.8 -        val rwrls = map mk_trans (List.concat(map mk_rew_rules thms));
     2.9 +        val new_rws = maps mk_rew_rules thms;
    2.10 +        val rwrls = map mk_trans (maps mk_rew_rules thms);
    2.11          val anet' = List.foldr lhs_insert_thm anet rwrls
    2.12      in  if !tracing andalso not(null new_rws)
    2.13          then writeln (cat_lines
    2.14 @@ -589,7 +589,7 @@
    2.15      val T' = Logic.incr_tvar 9 T;
    2.16  in mk_cong_type thy (Const(f,T'),T') end;
    2.17  
    2.18 -fun mk_congs thy = List.concat o map (mk_cong_thy thy);
    2.19 +fun mk_congs thy = maps (mk_cong_thy thy);
    2.20  
    2.21  fun mk_typed_congs thy =
    2.22  let
    2.23 @@ -599,7 +599,7 @@
    2.24        val t = case Sign.const_type thy f of
    2.25                    SOME(_) => Const(f,T) | NONE => Free(f,T)
    2.26      in (t,T) end
    2.27 -in List.concat o map (mk_cong_type thy o readfT) end;
    2.28 +in maps (mk_cong_type thy o readfT) end;
    2.29  
    2.30  end;
    2.31  end;
     3.1 --- a/src/HOL/Import/xml.ML	Thu Oct 15 23:10:35 2009 +0200
     3.2 +++ b/src/HOL/Import/xml.ML	Thu Oct 15 23:28:10 2009 +0200
     3.3 @@ -137,7 +137,7 @@
     3.4          || parse_pi >> K []
     3.5          || parse_comment >> K []) --
     3.6         Scan.optional ((* scan_whspc |-- *) parse_chars >> (single o Text)) []
     3.7 -         >> op @) >> List.concat) >> op @)(* --| scan_whspc*)) xs
     3.8 +         >> op @) >> flat) >> op @)(* --| scan_whspc*)) xs
     3.9  
    3.10  and parse_elem xs =
    3.11    ($$ "<" |-- scan_id --
     4.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Thu Oct 15 23:10:35 2009 +0200
     4.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Thu Oct 15 23:28:10 2009 +0200
     4.3 @@ -851,7 +851,7 @@
     4.4               val cps' = 
     4.5                  let fun cps'_fun ak1 ak2 = 
     4.6                  if ak1=ak2 then NONE else SOME (PureThy.get_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst"))
     4.7 -                in map (fn aki => (List.mapPartial I (map (cps'_fun aki) ak_names))) ak_names end;
     4.8 +                in map (fn aki => (map_filter I (map (cps'_fun aki) ak_names))) ak_names end;
     4.9               (* list of all dj_inst-theorems *)
    4.10               val djs = 
    4.11                 let fun djs_fun ak1 ak2 = 
    4.12 @@ -999,7 +999,7 @@
    4.13           prm_cons_thms ~~ prm_inst_thms ~~
    4.14           map (fn ths => Symtab.make (full_ak_names ~~ ths)) cp_thms ~~
    4.15           map (fn thss => Symtab.make
    4.16 -           (List.mapPartial (fn (s, [th]) => SOME (s, th) | _ => NONE)
    4.17 +           (map_filter (fn (s, [th]) => SOME (s, th) | _ => NONE)
    4.18                (full_ak_names ~~ thss))) dj_thms))) thy33
    4.19      end;
    4.20  
     5.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Thu Oct 15 23:10:35 2009 +0200
     5.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Thu Oct 15 23:28:10 2009 +0200
     5.3 @@ -45,18 +45,18 @@
     5.4  local
     5.5  
     5.6  fun dt_recs (DtTFree _) = []
     5.7 -  | dt_recs (DtType (_, dts)) = List.concat (map dt_recs dts)
     5.8 +  | dt_recs (DtType (_, dts)) = maps dt_recs dts
     5.9    | dt_recs (DtRec i) = [i];
    5.10  
    5.11  fun dt_cases (descr: descr) (_, args, constrs) =
    5.12    let
    5.13      fun the_bname i = Long_Name.base_name (#1 (valOf (AList.lookup (op =) descr i)));
    5.14 -    val bnames = map the_bname (distinct op = (List.concat (map dt_recs args)));
    5.15 +    val bnames = map the_bname (distinct op = (maps dt_recs args));
    5.16    in map (fn (c, _) => space_implode "_" (Long_Name.base_name c :: bnames)) constrs end;
    5.17  
    5.18  
    5.19  fun induct_cases descr =
    5.20 -  DatatypeProp.indexify_names (List.concat (map (dt_cases descr) (map #2 descr)));
    5.21 +  DatatypeProp.indexify_names (maps (dt_cases descr) (map #2 descr));
    5.22  
    5.23  fun exhaust_cases descr i = dt_cases descr (valOf (AList.lookup (op =) descr i));
    5.24  
    5.25 @@ -331,7 +331,7 @@
    5.26  
    5.27      val _ = warning "perm_empty_thms";
    5.28  
    5.29 -    val perm_empty_thms = List.concat (map (fn a =>
    5.30 +    val perm_empty_thms = maps (fn a =>
    5.31        let val permT = mk_permT (Type (a, []))
    5.32        in map standard (List.take (split_conj_thm
    5.33          (Goal.prove_global thy2 [] []
    5.34 @@ -347,7 +347,7 @@
    5.35              ALLGOALS (asm_full_simp_tac (global_simpset_of thy2))])),
    5.36          length new_type_names))
    5.37        end)
    5.38 -      atoms);
    5.39 +      atoms;
    5.40  
    5.41      (**** prove (pi1 @ pi2) \<bullet> t = pi1 \<bullet> (pi2 \<bullet> t) ****)
    5.42  
    5.43 @@ -357,7 +357,7 @@
    5.44      val at_pt_inst = PureThy.get_thm thy2 "at_pt_inst";
    5.45      val pt2 = PureThy.get_thm thy2 "pt2";
    5.46  
    5.47 -    val perm_append_thms = List.concat (map (fn a =>
    5.48 +    val perm_append_thms = maps (fn a =>
    5.49        let
    5.50          val permT = mk_permT (Type (a, []));
    5.51          val pi1 = Free ("pi1", permT);
    5.52 @@ -381,7 +381,7 @@
    5.53             (fn _ => EVERY [indtac induct perm_indnames 1,
    5.54                ALLGOALS (asm_full_simp_tac (global_simpset_of thy2 addsimps [pt2', pt2_ax]))]))),
    5.55           length new_type_names)
    5.56 -      end) atoms);
    5.57 +      end) atoms;
    5.58  
    5.59      (**** prove pi1 ~ pi2 ==> pi1 \<bullet> t = pi2 \<bullet> t ****)
    5.60  
    5.61 @@ -390,7 +390,7 @@
    5.62      val pt3 = PureThy.get_thm thy2 "pt3";
    5.63      val pt3_rev = PureThy.get_thm thy2 "pt3_rev";
    5.64  
    5.65 -    val perm_eq_thms = List.concat (map (fn a =>
    5.66 +    val perm_eq_thms = maps (fn a =>
    5.67        let
    5.68          val permT = mk_permT (Type (a, []));
    5.69          val pi1 = Free ("pi1", permT);
    5.70 @@ -417,7 +417,7 @@
    5.71             (fn _ => EVERY [indtac induct perm_indnames 1,
    5.72                ALLGOALS (asm_full_simp_tac (global_simpset_of thy2 addsimps [pt3', pt3_rev', pt3_ax]))]))),
    5.73           length new_type_names)
    5.74 -      end) atoms);
    5.75 +      end) atoms;
    5.76  
    5.77      (**** prove pi1 \<bullet> (pi2 \<bullet> t) = (pi1 \<bullet> pi2) \<bullet> (pi1 \<bullet> t) ****)
    5.78  
    5.79 @@ -506,7 +506,7 @@
    5.80      val rep_set_names = DatatypeProp.indexify_names
    5.81        (map (fn (i, _) => name_of_typ (nth_dtyp i) ^ "_set") descr);
    5.82      val big_rep_name =
    5.83 -      space_implode "_" (DatatypeProp.indexify_names (List.mapPartial
    5.84 +      space_implode "_" (DatatypeProp.indexify_names (map_filter
    5.85          (fn (i, ("Nominal.noption", _, _)) => NONE
    5.86            | (i, _) => SOME (name_of_typ (nth_dtyp i))) descr)) ^ "_set";
    5.87      val _ = warning ("big_rep_name: " ^ big_rep_name);
    5.88 @@ -521,8 +521,7 @@
    5.89        | strip_option dt = ([], dt);
    5.90  
    5.91      val dt_atomTs = distinct op = (map (typ_of_dtyp descr sorts)
    5.92 -      (List.concat (map (fn (_, (_, _, cs)) => List.concat
    5.93 -        (map (List.concat o map (fst o strip_option) o snd) cs)) descr)));
    5.94 +      (maps (fn (_, (_, _, cs)) => maps (maps (fst o strip_option) o snd) cs) descr));
    5.95      val dt_atoms = map (fst o dest_Type) dt_atomTs;
    5.96  
    5.97      fun make_intr s T (cname, cargs) =
    5.98 @@ -557,7 +556,7 @@
    5.99        end;
   5.100  
   5.101      val (intr_ts, (rep_set_names', recTs')) =
   5.102 -      apfst List.concat (apsnd ListPair.unzip (ListPair.unzip (List.mapPartial
   5.103 +      apfst flat (apsnd ListPair.unzip (ListPair.unzip (map_filter
   5.104          (fn ((_, ("Nominal.noption", _, _)), _) => NONE
   5.105            | ((i, (_, _, constrs)), rep_set_name) =>
   5.106                let val T = nth_dtyp i
   5.107 @@ -582,7 +581,7 @@
   5.108  
   5.109      val abs_perm = PureThy.get_thms thy4 "abs_perm";
   5.110  
   5.111 -    val perm_indnames' = List.mapPartial
   5.112 +    val perm_indnames' = map_filter
   5.113        (fn (x, (_, ("Nominal.noption", _, _))) => NONE | (x, _) => SOME x)
   5.114        (perm_indnames ~~ descr);
   5.115  
   5.116 @@ -861,8 +860,7 @@
   5.117              perm_closed_thms @ Rep_thms)) 1)
   5.118        end) Rep_thms;
   5.119  
   5.120 -    val perm_rep_perm_thms = List.concat (map prove_perm_rep_perm
   5.121 -      (atoms ~~ perm_closed_thmss));
   5.122 +    val perm_rep_perm_thms = maps prove_perm_rep_perm (atoms ~~ perm_closed_thmss);
   5.123  
   5.124      (* prove distinctness theorems *)
   5.125  
   5.126 @@ -887,7 +885,7 @@
   5.127  
   5.128      val perm_simps' = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) =>
   5.129        let val T = nth_dtyp' i
   5.130 -      in List.concat (map (fn (atom, perm_closed_thms) =>
   5.131 +      in maps (fn (atom, perm_closed_thms) =>
   5.132            map (fn ((cname, dts), constr_rep_thm) =>
   5.133          let
   5.134            val cname = Sign.intern_const thy8
   5.135 @@ -928,7 +926,7 @@
   5.136                 TRY (simp_tac (HOL_basic_ss addsimps
   5.137                   (perm_fun_def :: perm_defs @ Rep_thms @ Abs_inverse_thms @
   5.138                      perm_closed_thms)) 1)])
   5.139 -        end) (constrs ~~ constr_rep_thms)) (atoms ~~ perm_closed_thmss))
   5.140 +        end) (constrs ~~ constr_rep_thms)) (atoms ~~ perm_closed_thmss)
   5.141        end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss);
   5.142  
   5.143      (** prove injectivity of constructors **)
   5.144 @@ -943,7 +941,7 @@
   5.145  
   5.146      val inject_thms = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) =>
   5.147        let val T = nth_dtyp' i
   5.148 -      in List.mapPartial (fn ((cname, dts), constr_rep_thm) =>
   5.149 +      in map_filter (fn ((cname, dts), constr_rep_thm) =>
   5.150          if null dts then NONE else SOME
   5.151          let
   5.152            val cname = Sign.intern_const thy8
   5.153 @@ -986,7 +984,7 @@
   5.154      val (supp_thms, fresh_thms) = ListPair.unzip (map ListPair.unzip
   5.155        (map (fn ((((i, (_, _, constrs)), tname), inject_thms'), perm_thms') =>
   5.156        let val T = nth_dtyp' i
   5.157 -      in List.concat (map (fn (cname, dts) => map (fn atom =>
   5.158 +      in maps (fn (cname, dts) => map (fn atom =>
   5.159          let
   5.160            val cname = Sign.intern_const thy8
   5.161              (Long_Name.append tname (Long_Name.base_name cname));
   5.162 @@ -1028,7 +1026,7 @@
   5.163                  else foldr1 HOLogic.mk_conj (map fresh args2)))))
   5.164               (fn _ =>
   5.165                 simp_tac (HOL_ss addsimps [Un_iff, empty_iff, fresh_def, supp_thm]) 1))
   5.166 -        end) atoms) constrs)
   5.167 +        end) atoms) constrs
   5.168        end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ inject_thms ~~ perm_simps')));
   5.169  
   5.170      (**** weak induction theorem ****)
   5.171 @@ -1103,7 +1101,7 @@
   5.172              ALLGOALS (asm_full_simp_tac (global_simpset_of thy8 addsimps
   5.173                (abs_supp @ supp_atm @
   5.174                 PureThy.get_thms thy8 ("fs_" ^ Long_Name.base_name atom ^ "1") @
   5.175 -               List.concat supp_thms))))),
   5.176 +               flat supp_thms))))),
   5.177           length new_type_names))
   5.178        end) atoms;
   5.179  
   5.180 @@ -1156,9 +1154,9 @@
   5.181            mk_fresh1 (y :: xs) ys;
   5.182  
   5.183      fun mk_fresh2 xss [] = []
   5.184 -      | mk_fresh2 xss ((p as (ys, _)) :: yss) = List.concat (map (fn y as (_, T) =>
   5.185 +      | mk_fresh2 xss ((p as (ys, _)) :: yss) = maps (fn y as (_, T) =>
   5.186              map (fn (_, x as (_, U)) => HOLogic.mk_Trueprop
   5.187 -              (fresh_const T U $ Free y $ Free x)) (rev xss @ yss)) ys) @
   5.188 +              (fresh_const T U $ Free y $ Free x)) (rev xss @ yss)) ys @
   5.189            mk_fresh2 (p :: xss) yss;
   5.190  
   5.191      fun make_ind_prem fsT f k T ((cname, cargs), idxs) =
   5.192 @@ -1182,8 +1180,8 @@
   5.193  
   5.194          val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs');
   5.195          val prems' = map (fn p as (_, T) => HOLogic.mk_Trueprop
   5.196 -            (f T (Free p) (Free z))) (List.concat (map fst frees')) @
   5.197 -          mk_fresh1 [] (List.concat (map fst frees')) @
   5.198 +            (f T (Free p) (Free z))) (maps fst frees') @
   5.199 +          mk_fresh1 [] (maps fst frees') @
   5.200            mk_fresh2 [] frees'
   5.201  
   5.202        in list_all_free (frees @ [z], Logic.list_implies (prems' @ prems,
   5.203 @@ -1191,10 +1189,10 @@
   5.204            list_comb (Const (cname, Ts ---> T), map Free frees))))
   5.205        end;
   5.206  
   5.207 -    val ind_prems = List.concat (map (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
   5.208 +    val ind_prems = maps (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
   5.209        map (make_ind_prem fsT (fn T => fn t => fn u =>
   5.210          fresh_const T fsT $ t $ u) i T)
   5.211 -          (constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs));
   5.212 +          (constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs);
   5.213      val tnames = DatatypeProp.make_tnames recTs;
   5.214      val zs = Name.variant_list tnames (replicate (length descr'') "z");
   5.215      val ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
   5.216 @@ -1208,10 +1206,10 @@
   5.217          HOLogic.mk_Trueprop (Const ("Finite_Set.finite",
   5.218            (snd (split_last (binder_types T)) --> HOLogic.boolT) -->
   5.219              HOLogic.boolT) $ (f $ Free ("x", fsT'))))) fresh_fs @
   5.220 -      List.concat (map (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
   5.221 +      maps (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
   5.222          map (make_ind_prem fsT' (fn T => fn t => fn u => HOLogic.Not $
   5.223            HOLogic.mk_mem (t, the (AList.lookup op = fresh_fs T) $ u)) i T)
   5.224 -            (constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs));
   5.225 +            (constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs);
   5.226      val ind_concl' = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
   5.227        (map (fn ((((i, _), T), tname), z) =>
   5.228          make_pred fsT' i T $ Free (z, fsT') $ Free (tname, T))
   5.229 @@ -1448,10 +1446,10 @@
   5.230        Free (a, T --> HOLogic.boolT)) (pnames ~~ rec_result_Ts);
   5.231  
   5.232      fun mk_fresh3 rs [] = []
   5.233 -      | mk_fresh3 rs ((p as (ys, z)) :: yss) = List.concat (map (fn y as (_, T) =>
   5.234 -            List.mapPartial (fn ((_, (_, x)), r as (_, U)) => if z = x then NONE
   5.235 +      | mk_fresh3 rs ((p as (ys, z)) :: yss) = maps (fn y as (_, T) =>
   5.236 +            map_filter (fn ((_, (_, x)), r as (_, U)) => if z = x then NONE
   5.237                else SOME (HOLogic.mk_Trueprop
   5.238 -                (fresh_const T U $ Free y $ Free r))) rs) ys) @
   5.239 +                (fresh_const T U $ Free y $ Free r))) rs) ys @
   5.240            mk_fresh3 rs yss;
   5.241  
   5.242      (* FIXME: avoid collisions with other variable names? *)
   5.243 @@ -1463,9 +1461,9 @@
   5.244          val Ts = map (typ_of_dtyp descr'' sorts) cargs;
   5.245          val frees = map (fn i => "x" ^ string_of_int i) (1 upto length Ts) ~~ Ts;
   5.246          val frees' = partition_cargs idxs frees;
   5.247 -        val binders = List.concat (map fst frees');
   5.248 +        val binders = maps fst frees';
   5.249          val atomTs = distinct op = (maps (map snd o fst) frees');
   5.250 -        val recs = List.mapPartial
   5.251 +        val recs = map_filter
   5.252            (fn ((_, DtRec i), p) => SOME (i, p) | _ => NONE)
   5.253            (partition_cargs idxs cargs ~~ frees');
   5.254          val frees'' = map (fn i => "y" ^ string_of_int i) (1 upto length recs) ~~
   5.255 @@ -1490,14 +1488,14 @@
   5.256            fresh_const T (fastype_of result) $ Free p $ result) binders;
   5.257          val P = HOLogic.mk_Trueprop (p $ result)
   5.258        in
   5.259 -        (rec_intr_ts @ [Logic.list_implies (List.concat prems2 @ prems3 @ prems1,
   5.260 +        (rec_intr_ts @ [Logic.list_implies (flat prems2 @ prems3 @ prems1,
   5.261             HOLogic.mk_Trueprop (rec_set $
   5.262               list_comb (Const (cname, Ts ---> T), map Free frees) $ result))],
   5.263           rec_prems @ [list_all_free (frees @ frees'', Logic.list_implies (prems4, P))],
   5.264           rec_prems' @ map (fn fr => list_all_free (frees @ frees'',
   5.265             Logic.list_implies (List.nth (prems2, l) @ prems3 @ prems5 @ prems7 @ prems6 @ [P],
   5.266               HOLogic.mk_Trueprop fr))) result_freshs,
   5.267 -         rec_eq_prems @ [List.concat prems2 @ prems3],
   5.268 +         rec_eq_prems @ [flat prems2 @ prems3],
   5.269           l + 1)
   5.270        end;
   5.271  
   5.272 @@ -1709,7 +1707,7 @@
   5.273      val rec_unique_thms = split_conj_thm (Goal.prove
   5.274        (ProofContext.init thy11) (map fst rec_unique_frees)
   5.275        (map (augment_sort thy11 fs_cp_sort)
   5.276 -        (List.concat finite_premss @ finite_ctxt_prems @ rec_prems @ rec_prems'))
   5.277 +        (flat finite_premss @ finite_ctxt_prems @ rec_prems @ rec_prems'))
   5.278        (augment_sort thy11 fs_cp_sort
   5.279          (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj rec_unique_concls)))
   5.280        (fn {prems, context} =>
   5.281 @@ -1747,7 +1745,7 @@
   5.282                 (resolve_tac rec_intrs THEN_ALL_NEW atac) 1,
   5.283                 rotate_tac ~1 1,
   5.284                 ((DETERM o etac elim) THEN_ALL_NEW full_simp_tac
   5.285 -                  (HOL_ss addsimps List.concat distinct_thms)) 1] @
   5.286 +                  (HOL_ss addsimps flat distinct_thms)) 1] @
   5.287                 (if null idxs then [] else [hyp_subst_tac 1,
   5.288                  SUBPROOF (fn {asms, concl, prems = prems', params, context = context', ...} =>
   5.289                    let
   5.290 @@ -1758,10 +1756,10 @@
   5.291                      val rT = fastype_of lhs';
   5.292                      val (c, cargsl) = strip_comb lhs;
   5.293                      val cargsl' = partition_cargs idxs cargsl;
   5.294 -                    val boundsl = List.concat (map fst cargsl');
   5.295 +                    val boundsl = maps fst cargsl';
   5.296                      val (_, cargsr) = strip_comb rhs;
   5.297                      val cargsr' = partition_cargs idxs cargsr;
   5.298 -                    val boundsr = List.concat (map fst cargsr');
   5.299 +                    val boundsr = maps fst cargsr';
   5.300                      val (params1, _ :: params2) =
   5.301                        chop (length params div 2) (map (term_of o #2) params);
   5.302                      val params' = params1 @ params2;
   5.303 @@ -1779,8 +1777,7 @@
   5.304                      val _ = warning "step 1: obtaining fresh names";
   5.305                      val (freshs1, freshs2, context'') = fold
   5.306                        (obtain_fresh_name (rec_ctxt :: rec_fns' @ params')
   5.307 -                         (List.concat (map snd finite_thss) @
   5.308 -                            finite_ctxt_ths @ rec_prems)
   5.309 +                         (maps snd finite_thss @ finite_ctxt_ths @ rec_prems)
   5.310                           rec_fin_supp_thms')
   5.311                        Ts ([], [], context');
   5.312                      val pi1 = map perm_of_pair (boundsl ~~ freshs1);
   5.313 @@ -1794,7 +1791,7 @@
   5.314                      (** as, bs, cs # K as ts, K bs us **)
   5.315                      val _ = warning "step 2: as, bs, cs # K as ts, K bs us";
   5.316                      val prove_fresh_ss = HOL_ss addsimps
   5.317 -                      (finite_Diff :: List.concat fresh_thms @
   5.318 +                      (finite_Diff :: flat fresh_thms @
   5.319                         fs_atoms @ abs_fresh @ abs_supp @ fresh_atm);
   5.320                      (* FIXME: avoid asm_full_simp_tac ? *)
   5.321                      fun prove_fresh ths y x = Goal.prove context'' [] []
   5.322 @@ -1826,9 +1823,9 @@
   5.323                          (fn _ => EVERY
   5.324                             [cut_facts_tac [pi1_pi2_eq] 1,
   5.325                              asm_full_simp_tac (HOL_ss addsimps
   5.326 -                              (calc_atm @ List.concat perm_simps' @
   5.327 +                              (calc_atm @ flat perm_simps' @
   5.328                                 fresh_prems' @ freshs2' @ abs_perm @
   5.329 -                               alpha @ List.concat inject_thms)) 1]))
   5.330 +                               alpha @ flat inject_thms)) 1]))
   5.331                          (map snd cargsl' ~~ map snd cargsr');
   5.332  
   5.333                      (** pi1^-1 o pi2 o us = ts **)
   5.334 @@ -1896,13 +1893,13 @@
   5.335  
   5.336                      (** as # rs **)
   5.337                      val _ = warning "step 8: as # rs";
   5.338 -                    val rec_freshs = List.concat
   5.339 -                      (map (fn (rec_prem, ih) =>
   5.340 +                    val rec_freshs =
   5.341 +                      maps (fn (rec_prem, ih) =>
   5.342                          let
   5.343                            val _ $ (S $ x $ (y as Free (_, T))) =
   5.344                              prop_of rec_prem;
   5.345                            val k = find_index (equal S) rec_sets;
   5.346 -                          val atoms = List.concat (List.mapPartial (fn (bs, z) =>
   5.347 +                          val atoms = flat (map_filter (fn (bs, z) =>
   5.348                              if z = x then NONE else SOME bs) cargsl')
   5.349                          in
   5.350                            map (fn a as Free (_, aT) =>
   5.351 @@ -1917,7 +1914,7 @@
   5.352                                      [rtac rec_prem 1, rtac ih 1,
   5.353                                       REPEAT_DETERM (resolve_tac fresh_prems 1)]))
   5.354                              end) atoms
   5.355 -                        end) (rec_prems1 ~~ ihs));
   5.356 +                        end) (rec_prems1 ~~ ihs);
   5.357  
   5.358                      (** as # fK as ts rs , bs # fK bs us vs **)
   5.359                      val _ = warning "step 9: as # fK as ts rs , bs # fK bs us vs";
   5.360 @@ -1969,7 +1966,7 @@
   5.361                             NominalPermeq.fresh_guess_tac
   5.362                               (HOL_ss addsimps (freshs2 @
   5.363                                  fs_atoms @ fresh_atm @
   5.364 -                                List.concat (map snd finite_thss))) 1]);
   5.365 +                                maps snd finite_thss)) 1]);
   5.366  
   5.367                      val fresh_results' =
   5.368                        map (prove_fresh_result' rec_prems1 rhs') freshs1 @
   5.369 @@ -2031,7 +2028,7 @@
   5.370          val ps = map (fn (x as Free (_, T), i) =>
   5.371            (Free ("x" ^ string_of_int i, T), x)) (cargs ~~ (1 upto length cargs));
   5.372          val concl' = subst_atomic_types (rec_result_Ts' ~~ rec_result_Ts) concl;
   5.373 -        val prems' = List.concat finite_premss @ finite_ctxt_prems @
   5.374 +        val prems' = flat finite_premss @ finite_ctxt_prems @
   5.375            rec_prems @ rec_prems' @ map (subst_atomic ps) prems;
   5.376          fun solve rules prems = resolve_tac rules THEN_ALL_NEW
   5.377            (resolve_tac prems THEN_ALL_NEW atac)
   5.378 @@ -2054,10 +2051,10 @@
   5.379      (* FIXME: theorems are stored in database for testing only *)
   5.380      val (_, thy13) = thy12 |>
   5.381        PureThy.add_thmss
   5.382 -        [((Binding.name "rec_equiv", List.concat rec_equiv_thms), []),
   5.383 -         ((Binding.name "rec_equiv'", List.concat rec_equiv_thms'), []),
   5.384 -         ((Binding.name "rec_fin_supp", List.concat rec_fin_supp_thms), []),
   5.385 -         ((Binding.name "rec_fresh", List.concat rec_fresh_thms), []),
   5.386 +        [((Binding.name "rec_equiv", flat rec_equiv_thms), []),
   5.387 +         ((Binding.name "rec_equiv'", flat rec_equiv_thms'), []),
   5.388 +         ((Binding.name "rec_fin_supp", flat rec_fin_supp_thms), []),
   5.389 +         ((Binding.name "rec_fresh", flat rec_fresh_thms), []),
   5.390           ((Binding.name "rec_unique", map standard rec_unique_thms), []),
   5.391           ((Binding.name "recs", rec_thms), [])] ||>
   5.392        Sign.parent_path ||>
     6.1 --- a/src/HOL/Nominal/nominal_induct.ML	Thu Oct 15 23:10:35 2009 +0200
     6.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Thu Oct 15 23:28:10 2009 +0200
     6.3 @@ -50,10 +50,10 @@
     6.4        in
     6.5          (P, tuple_fun (map #2 avoiding) (Term.dest_Var P)) ::
     6.6          (x, tuple (map Free avoiding)) ::
     6.7 -        List.mapPartial (fn (z, SOME t) => SOME (z, t) | _ => NONE) (zs ~~ inst)
     6.8 +        map_filter (fn (z, SOME t) => SOME (z, t) | _ => NONE) (zs ~~ inst)
     6.9        end;
    6.10       val substs =
    6.11 -       map2 subst insts concls |> List.concat |> distinct (op =)
    6.12 +       map2 subst insts concls |> flat |> distinct (op =)
    6.13         |> map (pairself (Thm.cterm_of (ProofContext.theory_of ctxt)));
    6.14    in 
    6.15      (((cases, nconcls), consumes), Drule.cterm_instantiate substs joined_rule) 
    6.16 @@ -98,7 +98,7 @@
    6.17      (fn i => fn st =>
    6.18        rules
    6.19        |> inst_mutual_rule ctxt insts avoiding
    6.20 -      |> RuleCases.consume (List.concat defs) facts
    6.21 +      |> RuleCases.consume (flat defs) facts
    6.22        |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
    6.23          (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
    6.24            (CONJUNCTS (ALLGOALS
     7.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Thu Oct 15 23:10:35 2009 +0200
     7.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Thu Oct 15 23:28:10 2009 +0200
     7.3 @@ -224,7 +224,7 @@
     7.4        | lift_prem t = t;
     7.5  
     7.6      fun mk_distinct [] = []
     7.7 -      | mk_distinct ((x, T) :: xs) = List.mapPartial (fn (y, U) =>
     7.8 +      | mk_distinct ((x, T) :: xs) = map_filter (fn (y, U) =>
     7.9            if T = U then SOME (HOLogic.mk_Trueprop
    7.10              (HOLogic.mk_not (HOLogic.eq_const T $ x $ y)))
    7.11            else NONE) xs @ mk_distinct xs;
    7.12 @@ -263,7 +263,7 @@
    7.13  
    7.14      val vc_compat = map (fn (params, bvars, prems, (p, ts)) =>
    7.15        map (fn q => list_all (params, incr_boundvars ~1 (Logic.list_implies
    7.16 -          (List.mapPartial (fn prem =>
    7.17 +          (map_filter (fn prem =>
    7.18               if null (preds_of ps prem) then SOME prem
    7.19               else map_term (split_conj (K o I) names) prem prem) prems, q))))
    7.20          (mk_distinct bvars @
    7.21 @@ -359,7 +359,7 @@
    7.22                             (etac conjunct1 1) monos NONE th,
    7.23                           mk_pi (the (map_thm ctxt (inst_conj_all names ps (rev pis''))
    7.24                             (inst_conj_all_tac (length pis'')) monos (SOME t) th))))
    7.25 -                      (gprems ~~ oprems)) |>> List.mapPartial I;
    7.26 +                      (gprems ~~ oprems)) |>> map_filter I;
    7.27                   val vc_compat_ths' = map (fn th =>
    7.28                     let
    7.29                       val th' = first_order_mrs gprems1 th;
     8.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Thu Oct 15 23:10:35 2009 +0200
     8.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Thu Oct 15 23:28:10 2009 +0200
     8.3 @@ -279,7 +279,7 @@
     8.4  
     8.5      val (vc_compat, vc_compat') = map (fn (params, sets, prems, (p, ts)) =>
     8.6        map (fn q => abs_params params (incr_boundvars ~1 (Logic.list_implies
     8.7 -          (List.mapPartial (fn prem =>
     8.8 +          (map_filter (fn prem =>
     8.9               if null (preds_of ps prem) then SOME prem
    8.10               else map_term (split_conj (K o I) names) prem prem) prems, q))))
    8.11          (maps (fn (t, T) => map (fn (u, U) => HOLogic.mk_Trueprop
    8.12 @@ -366,7 +366,7 @@
    8.13                   val pi_sets = map (fn (t, _) =>
    8.14                     fold_rev (NominalDatatype.mk_perm []) pis t) sets';
    8.15                   val (P, ts) = strip_comb (HOLogic.dest_Trueprop (term_of concl));
    8.16 -                 val gprems1 = List.mapPartial (fn (th, t) =>
    8.17 +                 val gprems1 = map_filter (fn (th, t) =>
    8.18                     if null (preds_of ps t) then SOME th
    8.19                     else
    8.20                       map_thm ctxt' (split_conj (K o I) names)
     9.1 --- a/src/HOL/Product_Type.thy	Thu Oct 15 23:10:35 2009 +0200
     9.2 +++ b/src/HOL/Product_Type.thy	Thu Oct 15 23:28:10 2009 +0200
     9.3 @@ -1017,7 +1017,7 @@
     9.4                (Codegen.invoke_codegen thy defs dep thyname true) ts gr2
     9.5            in
     9.6              SOME (Codegen.mk_app brack
     9.7 -              (Pretty.blk (0, [Codegen.str "let ", Pretty.blk (0, List.concat
     9.8 +              (Pretty.blk (0, [Codegen.str "let ", Pretty.blk (0, flat
     9.9                    (separate [Codegen.str ";", Pretty.brk 1] (map (fn (pl, pr) =>
    9.10                      [Pretty.block [Codegen.str "val ", pl, Codegen.str " =",
    9.11                         Pretty.brk 1, pr]]) qs))),
    10.1 --- a/src/HOL/Prolog/prolog.ML	Thu Oct 15 23:10:35 2009 +0200
    10.2 +++ b/src/HOL/Prolog/prolog.ML	Thu Oct 15 23:28:10 2009 +0200
    10.3 @@ -106,7 +106,7 @@
    10.4          in Library.foldl (op APPEND) (no_tac, ptacs) st end;
    10.5  
    10.6  fun ptac ctxt prog = let
    10.7 -  val proga = List.concat (map (atomizeD ctxt) prog)                   (* atomize the prog *)
    10.8 +  val proga = maps (atomizeD ctxt) prog         (* atomize the prog *)
    10.9    in    (REPEAT_DETERM1 o FIRST' [
   10.10                  rtac TrueI,                     (* "True" *)
   10.11                  rtac conjI,                     (* "[| P; Q |] ==> P & Q" *)
    11.1 --- a/src/HOL/Statespace/state_fun.ML	Thu Oct 15 23:10:35 2009 +0200
    11.2 +++ b/src/HOL/Statespace/state_fun.ML	Thu Oct 15 23:28:10 2009 +0200
    11.3 @@ -333,7 +333,7 @@
    11.4      [] => ""
    11.5     | c::cs => String.implode (Char.toUpper c::cs ))
    11.6  
    11.7 -fun mkName (Type (T,args)) = concat (map mkName args) ^ mkUpper (Long_Name.base_name T)
    11.8 +fun mkName (Type (T,args)) = implode (map mkName args) ^ mkUpper (Long_Name.base_name T)
    11.9    | mkName (TFree (x,_)) = mkUpper (Long_Name.base_name x)
   11.10    | mkName (TVar ((x,_),_)) = mkUpper (Long_Name.base_name x);
   11.11  
   11.12 @@ -347,7 +347,7 @@
   11.13    | gen_constr_destr comp prfx thy (T as Type ("fun",_)) =
   11.14       let val (argTs,rangeT) = strip_type T;
   11.15       in comp 
   11.16 -          (Syntax.const (deco prfx (concat (map mkName argTs) ^ "Fun")))
   11.17 +          (Syntax.const (deco prfx (implode (map mkName argTs) ^ "Fun")))
   11.18            (fold (fn x => fn y => x$y)
   11.19                 (replicate (length argTs) (Syntax.const "StateFun.map_fun"))
   11.20                 (gen_constr_destr comp prfx thy rangeT))
   11.21 @@ -361,7 +361,7 @@
   11.22                       ((mk_map T $ gen_constr_destr comp prfx thy argT))
   11.23            | _ => raise (TYPE ("StateFun.gen_constr_destr",[T'],[])))
   11.24       else (* type args are not recursively embedded into val *)
   11.25 -           Syntax.const (deco prfx (concat (map mkName argTs) ^ mkUpper (Long_Name.base_name T)))
   11.26 +           Syntax.const (deco prfx (implode (map mkName argTs) ^ mkUpper (Long_Name.base_name T)))
   11.27    | gen_constr_destr thy _ _ T = raise (TYPE ("StateFun.gen_constr_destr",[T],[]));
   11.28                     
   11.29  val mk_constr = gen_constr_destr (fn a => fn b => Syntax.const "Fun.comp" $ a $ b) ""
    12.1 --- a/src/HOL/Statespace/state_space.ML	Thu Oct 15 23:10:35 2009 +0200
    12.2 +++ b/src/HOL/Statespace/state_space.ML	Thu Oct 15 23:28:10 2009 +0200
    12.3 @@ -369,7 +369,7 @@
    12.4      val inst = map fst args ~~ Ts;
    12.5      val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst);
    12.6      val parent_comps =
    12.7 -     List.concat (map (fn (Ts',n,rs) => parent_components thy (map subst Ts',n,rs)) parents);
    12.8 +      maps (fn (Ts',n,rs) => parent_components thy (map subst Ts',n,rs)) parents;
    12.9      val all_comps = rename renaming (parent_comps @ map (apsnd subst) components);
   12.10    in all_comps end;
   12.11  
   12.12 @@ -403,10 +403,9 @@
   12.13                      (("",false),Expression.Positional 
   12.14                               [SOME (Free (project_name T,projectT T)), 
   12.15                                SOME (Free ((inject_name T,injectT T)))]))) Ts;
   12.16 -    val locs = flat (map (fn T => [(Binding.name (project_name T),NONE,NoSyn),
   12.17 -                                     (Binding.name (inject_name T),NONE,NoSyn)]) Ts);
   12.18 -    val constrains = List.concat
   12.19 -         (map (fn T => [(project_name T,projectT T),(inject_name T,injectT T)]) Ts);
   12.20 +    val locs = maps (fn T => [(Binding.name (project_name T),NONE,NoSyn),
   12.21 +                                     (Binding.name (inject_name T),NONE,NoSyn)]) Ts;
   12.22 +    val constrains = maps (fn T => [(project_name T,projectT T),(inject_name T,injectT T)]) Ts;
   12.23  
   12.24      fun interprete_parent_valuetypes (Ts, pname, _) thy =
   12.25        let
   12.26 @@ -414,7 +413,7 @@
   12.27               the (Symtab.lookup (StateSpaceData.get (Context.Theory thy)) pname);
   12.28          val inst = map fst args ~~ Ts;
   12.29          val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst);
   12.30 -        val pars = List.concat (map ((fn T => [project_name T,inject_name T]) o subst) types);
   12.31 +        val pars = maps ((fn T => [project_name T,inject_name T]) o subst) types;
   12.32  
   12.33          val expr = ([(suffix valuetypesN name, 
   12.34                       (("",false),Expression.Positional (map SOME pars)))],[]);
   12.35 @@ -562,7 +561,7 @@
   12.36      fun fst_eq ((x:string,_),(y,_)) = x = y;
   12.37      fun snd_eq ((_,t:typ),(_,u)) = t = u;
   12.38  
   12.39 -    val raw_parent_comps = (List.concat (map (parent_components thy) parents'));
   12.40 +    val raw_parent_comps = maps (parent_components thy) parents';
   12.41      fun check_type (n,T) =
   12.42            (case distinct (snd_eq) (filter (curry fst_eq (n,T)) raw_parent_comps) of
   12.43               []  => []
   12.44 @@ -570,7 +569,7 @@
   12.45             | rs  => ["Different types for component " ^ n ^": " ^
   12.46                  commas (map (Syntax.string_of_typ ctxt o snd) rs)])
   12.47  
   12.48 -    val err_dup_types = List.concat (map check_type (duplicates fst_eq raw_parent_comps))
   12.49 +    val err_dup_types = maps check_type (duplicates fst_eq raw_parent_comps)
   12.50  
   12.51      val parent_comps = distinct (fst_eq) raw_parent_comps;
   12.52      val all_comps = parent_comps @ comps';
    13.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Oct 15 23:10:35 2009 +0200
    13.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Oct 15 23:28:10 2009 +0200
    13.3 @@ -49,7 +49,7 @@
    13.4    let
    13.5      val _ = message config "Proving case distinction theorems ...";
    13.6  
    13.7 -    val descr' = List.concat descr;
    13.8 +    val descr' = flat descr;
    13.9      val recTs = get_rec_types descr' sorts;
   13.10      val newTs = Library.take (length (hd descr), recTs);
   13.11  
   13.12 @@ -95,7 +95,7 @@
   13.13      val big_name = space_implode "_" new_type_names;
   13.14      val thy0 = Sign.add_path big_name thy;
   13.15  
   13.16 -    val descr' = List.concat descr;
   13.17 +    val descr' = flat descr;
   13.18      val recTs = get_rec_types descr' sorts;
   13.19      val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
   13.20      val newTs = Library.take (length (hd descr), recTs);
   13.21 @@ -278,7 +278,7 @@
   13.22  
   13.23      val thy1 = Sign.add_path (space_implode "_" new_type_names) thy;
   13.24  
   13.25 -    val descr' = List.concat descr;
   13.26 +    val descr' = flat descr;
   13.27      val recTs = get_rec_types descr' sorts;
   13.28      val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
   13.29      val newTs = Library.take (length (hd descr), recTs);
   13.30 @@ -312,14 +312,14 @@
   13.31              end) (constrs ~~ (1 upto length constrs)));
   13.32  
   13.33            val caseT = (map (snd o dest_Free) fns1) @ [T] ---> T';
   13.34 -          val fns = (List.concat (Library.take (i, case_dummy_fns))) @
   13.35 -            fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns)));
   13.36 +          val fns = flat (Library.take (i, case_dummy_fns)) @
   13.37 +            fns2 @ flat (Library.drop (i + 1, case_dummy_fns));
   13.38            val reccomb = Const (recname, (map fastype_of fns) @ [T] ---> T');
   13.39            val decl = ((Binding.name (Long_Name.base_name name), caseT), NoSyn);
   13.40            val def = (Binding.name (Long_Name.base_name name ^ "_def"),
   13.41              Logic.mk_equals (list_comb (Const (name, caseT), fns1),
   13.42 -              list_comb (reccomb, (List.concat (Library.take (i, case_dummy_fns))) @
   13.43 -                fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns))) )));
   13.44 +              list_comb (reccomb, (flat (Library.take (i, case_dummy_fns))) @
   13.45 +                fns2 @ (flat (Library.drop (i + 1, case_dummy_fns))) )));
   13.46            val ([def_thm], thy') =
   13.47              thy
   13.48              |> Sign.declare_const [] decl |> snd
    14.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Thu Oct 15 23:10:35 2009 +0200
    14.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Thu Oct 15 23:28:10 2009 +0200
    14.3 @@ -124,7 +124,7 @@
    14.4            | _ => NONE)
    14.5        | SOME (_ $ t') => SOME (Abs ("x", fastype_of t', abstract_over (t', t2))))
    14.6      val cert = cterm_of (Thm.theory_of_thm st);
    14.7 -    val insts = List.mapPartial (fn (t, u) => case abstr (getP u) of
    14.8 +    val insts = map_filter (fn (t, u) => case abstr (getP u) of
    14.9          NONE => NONE
   14.10        | SOME u' => SOME (t |> getP |> snd |> head_of |> cert, cert u')) (ts ~~ ts');
   14.11      val indrule' = cterm_instantiate insts indrule
   14.12 @@ -279,7 +279,7 @@
   14.13  
   14.14  fun check_nonempty descr =
   14.15    let
   14.16 -    val descr' = List.concat descr;
   14.17 +    val descr' = flat descr;
   14.18      fun is_nonempty_dt is i =
   14.19        let
   14.20          val (_, _, constrs) = (the o AList.lookup (op =) descr') i;
    15.1 --- a/src/HOL/Tools/Datatype/datatype_case.ML	Thu Oct 15 23:10:35 2009 +0200
    15.2 +++ b/src/HOL/Tools/Datatype/datatype_case.ML	Thu Oct 15 23:28:10 2009 +0200
    15.3 @@ -241,8 +241,7 @@
    15.4                    val types = map type_of (case_functions @ [u]);
    15.5                    val case_const = Const (case_name, types ---> range_ty)
    15.6                    val tree = list_comb (case_const, case_functions @ [u])
    15.7 -                  val pat_rect1 = flat (map mk_pat
    15.8 -                    (constructors ~~ constructors' ~~ pat_rect))
    15.9 +                  val pat_rect1 = maps mk_pat (constructors ~~ constructors' ~~ pat_rect)
   15.10                  in (pat_rect1, tree)
   15.11                  end)
   15.12              | SOME (t, i) => raise CASE_ERROR ("Not a datatype constructor: " ^
    16.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Thu Oct 15 23:10:35 2009 +0200
    16.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Thu Oct 15 23:28:10 2009 +0200
    16.3 @@ -69,17 +69,17 @@
    16.4                 (if null tvs then [] else
    16.5                    [mk_tuple (map str tvs), str " "]) @
    16.6                 [str (type_id ^ " ="), Pretty.brk 1] @
    16.7 -               List.concat (separate [Pretty.brk 1, str "| "]
    16.8 +               flat (separate [Pretty.brk 1, str "| "]
    16.9                   (map (fn (ps', (_, cname)) => [Pretty.block
   16.10                     (str cname ::
   16.11                      (if null ps' then [] else
   16.12 -                     List.concat ([str " of", Pretty.brk 1] ::
   16.13 +                     flat ([str " of", Pretty.brk 1] ::
   16.14                         separate [str " *", Pretty.brk 1]
   16.15                           (map single ps'))))]) ps))) :: rest, gr''')
   16.16            end;
   16.17  
   16.18      fun mk_constr_term cname Ts T ps =
   16.19 -      List.concat (separate [str " $", Pretty.brk 1]
   16.20 +      flat (separate [str " $", Pretty.brk 1]
   16.21          ([str ("Const (\"" ^ cname ^ "\","), Pretty.brk 1,
   16.22            mk_type false (Ts ---> T), str ")"] :: ps));
   16.23  
   16.24 @@ -148,7 +148,7 @@
   16.25              fun mk_choice [c] = mk_constr "(i-1)" false c
   16.26                | mk_choice cs = Pretty.block [str "one_of",
   16.27                    Pretty.brk 1, Pretty.blk (1, str "[" ::
   16.28 -                  List.concat (separate [str ",", Pretty.fbrk]
   16.29 +                  flat (separate [str ",", Pretty.fbrk]
   16.30                      (map (single o mk_delay o mk_constr "(i-1)" false) cs)) @
   16.31                    [str "]"]), Pretty.brk 1, str "()"];
   16.32  
   16.33 @@ -242,7 +242,7 @@
   16.34                end;
   16.35  
   16.36          val (ps1, gr1) = pcase constrs ts1 Ts gr ;
   16.37 -        val ps = List.concat (separate [Pretty.brk 1, str "| "] ps1);
   16.38 +        val ps = flat (separate [Pretty.brk 1, str "| "] ps1);
   16.39          val (p, gr2) = invoke_codegen thy defs dep module false t gr1;
   16.40          val (ps2, gr3) = fold_map (invoke_codegen thy defs dep module true) ts2 gr2;
   16.41        in ((if not (null ts2) andalso brack then parens else I)
    17.1 --- a/src/HOL/Tools/Datatype/datatype_prop.ML	Thu Oct 15 23:10:35 2009 +0200
    17.2 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Thu Oct 15 23:28:10 2009 +0200
    17.3 @@ -113,7 +113,7 @@
    17.4  
    17.5  fun make_ind descr sorts =
    17.6    let
    17.7 -    val descr' = List.concat descr;
    17.8 +    val descr' = flat descr;
    17.9      val recTs = get_rec_types descr' sorts;
   17.10      val pnames = if length descr' = 1 then ["P"]
   17.11        else map (fn i => "P" ^ string_of_int i) (1 upto length descr');
   17.12 @@ -143,8 +143,8 @@
   17.13            list_comb (Const (cname, Ts ---> T), map Free frees))))
   17.14        end;
   17.15  
   17.16 -    val prems = List.concat (map (fn ((i, (_, _, constrs)), T) =>
   17.17 -      map (make_ind_prem i T) constrs) (descr' ~~ recTs));
   17.18 +    val prems = maps (fn ((i, (_, _, constrs)), T) =>
   17.19 +      map (make_ind_prem i T) constrs) (descr' ~~ recTs);
   17.20      val tnames = make_tnames recTs;
   17.21      val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
   17.22        (map (fn (((i, _), T), tname) => make_pred i T $ Free (tname, T))
   17.23 @@ -156,7 +156,7 @@
   17.24  
   17.25  fun make_casedists descr sorts =
   17.26    let
   17.27 -    val descr' = List.concat descr;
   17.28 +    val descr' = flat descr;
   17.29  
   17.30      fun make_casedist_prem T (cname, cargs) =
   17.31        let
   17.32 @@ -181,12 +181,12 @@
   17.33  
   17.34  fun make_primrec_Ts descr sorts used =
   17.35    let
   17.36 -    val descr' = List.concat descr;
   17.37 +    val descr' = flat descr;
   17.38  
   17.39      val rec_result_Ts = map TFree (Name.variant_list used (replicate (length descr') "'t") ~~
   17.40        replicate (length descr') HOLogic.typeS);
   17.41  
   17.42 -    val reccomb_fn_Ts = List.concat (map (fn (i, (_, _, constrs)) =>
   17.43 +    val reccomb_fn_Ts = maps (fn (i, (_, _, constrs)) =>
   17.44        map (fn (_, cargs) =>
   17.45          let
   17.46            val Ts = map (typ_of_dtyp descr' sorts) cargs;
   17.47 @@ -197,13 +197,13 @@
   17.48  
   17.49            val argTs = Ts @ map mk_argT recs
   17.50          in argTs ---> List.nth (rec_result_Ts, i)
   17.51 -        end) constrs) descr');
   17.52 +        end) constrs) descr';
   17.53  
   17.54    in (rec_result_Ts, reccomb_fn_Ts) end;
   17.55  
   17.56  fun make_primrecs new_type_names descr sorts thy =
   17.57    let
   17.58 -    val descr' = List.concat descr;
   17.59 +    val descr' = flat descr;
   17.60      val recTs = get_rec_types descr' sorts;
   17.61      val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
   17.62  
   17.63 @@ -253,7 +253,7 @@
   17.64  
   17.65  fun make_case_combs new_type_names descr sorts thy fname =
   17.66    let
   17.67 -    val descr' = List.concat descr;
   17.68 +    val descr' = flat descr;
   17.69      val recTs = get_rec_types descr' sorts;
   17.70      val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
   17.71      val newTs = Library.take (length (hd descr), recTs);
   17.72 @@ -277,7 +277,7 @@
   17.73  
   17.74  fun make_cases new_type_names descr sorts thy =
   17.75    let
   17.76 -    val descr' = List.concat descr;
   17.77 +    val descr' = flat descr;
   17.78      val recTs = get_rec_types descr' sorts;
   17.79      val newTs = Library.take (length (hd descr), recTs);
   17.80  
   17.81 @@ -300,7 +300,7 @@
   17.82  
   17.83  fun make_splits new_type_names descr sorts thy =
   17.84    let
   17.85 -    val descr' = List.concat descr;
   17.86 +    val descr' = flat descr;
   17.87      val recTs = get_rec_types descr' sorts;
   17.88      val used' = List.foldr OldTerm.add_typ_tfree_names [] recTs;
   17.89      val newTs = Library.take (length (hd descr), recTs);
   17.90 @@ -412,7 +412,7 @@
   17.91  
   17.92  fun make_nchotomys descr sorts =
   17.93    let
   17.94 -    val descr' = List.concat descr;
   17.95 +    val descr' = flat descr;
   17.96      val recTs = get_rec_types descr' sorts;
   17.97      val newTs = Library.take (length (hd descr), recTs);
   17.98  
    18.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Thu Oct 15 23:10:35 2009 +0200
    18.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Thu Oct 15 23:28:10 2009 +0200
    18.3 @@ -103,7 +103,7 @@
    18.4        (list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Bound 0) (Bound 0)))
    18.5          (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names);
    18.6      val r = if null is then Extraction.nullt else
    18.7 -      foldr1 HOLogic.mk_prod (List.mapPartial (fn (((((i, _), T), U), s), tname) =>
    18.8 +      foldr1 HOLogic.mk_prod (map_filter (fn (((((i, _), T), U), s), tname) =>
    18.9          if i mem is then SOME
   18.10            (list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Free (tname, T))
   18.11          else NONE) (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names ~~ tnames));
    19.1 --- a/src/HOL/Tools/Function/fundef.ML	Thu Oct 15 23:10:35 2009 +0200
    19.2 +++ b/src/HOL/Tools/Function/fundef.ML	Thu Oct 15 23:28:10 2009 +0200
    19.3 @@ -58,7 +58,7 @@
    19.4        val (saved_spec_simps, lthy) =
    19.5          fold_map (LocalTheory.note Thm.generatedK) spec lthy
    19.6  
    19.7 -      val saved_simps = flat (map snd saved_spec_simps)
    19.8 +      val saved_simps = maps snd saved_spec_simps
    19.9        val simps_by_f = sort saved_simps
   19.10  
   19.11        fun add_for_f fname simps =
    20.1 --- a/src/HOL/Tools/Function/lexicographic_order.ML	Thu Oct 15 23:10:35 2009 +0200
    20.2 +++ b/src/HOL/Tools/Function/lexicographic_order.ML	Thu Oct 15 23:28:10 2009 +0200
    20.3 @@ -137,7 +137,7 @@
    20.4  
    20.5  (** Error reporting **)
    20.6  
    20.7 -fun pr_table table = writeln (cat_lines (map (fn r => concat (map pr_cell r)) table))
    20.8 +fun pr_table table = writeln (cat_lines (map (fn r => implode (map pr_cell r)) table))
    20.9  
   20.10  fun pr_goals ctxt st =
   20.11      Goal_Display.pretty_goals ctxt {total = true, main = false, maxgoals = Thm.nprems_of st} st
   20.12 @@ -176,8 +176,8 @@
   20.13  
   20.14        val gc = map (fn i => chr (i + 96)) (1 upto length table)
   20.15        val mc = 1 upto length measure_funs
   20.16 -      val tstr = "Result matrix:" ::  ("   " ^ concat (map (enclose " " " " o string_of_int) mc))
   20.17 -                 :: map2 (fn r => fn i => i ^ ": " ^ concat (map pr_cell r)) table gc
   20.18 +      val tstr = "Result matrix:" ::  ("   " ^ implode (map (enclose " " " " o string_of_int) mc))
   20.19 +                 :: map2 (fn r => fn i => i ^ ": " ^ implode (map pr_cell r)) table gc
   20.20        val gstr = "Calls:" :: map2 (prefix "  " oo pr_goal) tl gc
   20.21        val mstr = "Measures:" :: map2 (prefix "  " oo pr_fun) measure_funs mc
   20.22        val ustr = "Unfinished subgoals:" :: pr_unprovable_subgoals ctxt table
    21.1 --- a/src/HOL/Tools/Function/pattern_split.ML	Thu Oct 15 23:10:35 2009 +0200
    21.2 +++ b/src/HOL/Tools/Function/pattern_split.ML	Thu Oct 15 23:28:10 2009 +0200
    21.3 @@ -70,7 +70,7 @@
    21.4                    map (fn (vs, subst) => (vs, (v,t)::subst)) substs
    21.5                  end
    21.6            in
    21.7 -            flat (map foo (inst_constrs_of (ProofContext.theory_of ctx) T))
    21.8 +            maps foo (inst_constrs_of (ProofContext.theory_of ctx) T)
    21.9            end
   21.10          | pattern_subtract_subst_aux vs t t' =
   21.11            let
   21.12 @@ -110,7 +110,7 @@
   21.13  
   21.14  (* ps - p' *)
   21.15  fun pattern_subtract_from_many ctx p'=
   21.16 -    flat o map (pattern_subtract ctx p')
   21.17 +    maps (pattern_subtract ctx p')
   21.18  
   21.19  (* in reverse order *)
   21.20  fun pattern_subtract_many ctx ps' =
    22.1 --- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Thu Oct 15 23:10:35 2009 +0200
    22.2 +++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Thu Oct 15 23:28:10 2009 +0200
    22.3 @@ -316,7 +316,7 @@
    22.4      fun index xs = (1 upto length xs) ~~ xs
    22.5      fun outp s t f xs = map (fn (x, y) => s ^ Int.toString x ^ t ^ f y ^ "\n") xs
    22.6      val ims = index (map index ms)
    22.7 -    val _ = tracing (concat (outp "fn #" ":\n" (concat o outp "\tmeasure #" ": " (Syntax.string_of_term ctxt)) ims))
    22.8 +    val _ = tracing (implode (outp "fn #" ":\n" (implode o outp "\tmeasure #" ": " (Syntax.string_of_term ctxt)) ims))
    22.9      fun print_call (k, c) =
   22.10        let
   22.11          val (_, p, _, q, _, _) = dest_call D c
   22.12 @@ -325,8 +325,8 @@
   22.13          val caller_ms = nth ms p
   22.14          val callee_ms = nth ms q
   22.15          val entries = map (fn x => map (pair x) (callee_ms)) (caller_ms)
   22.16 -        fun print_ln (i : int, l) = concat (Int.toString i :: "   " :: map (enclose " " " " o print_cell o (uncurry (get_descent D c))) l)
   22.17 -        val _ = tracing (concat (Int.toString (p + 1) ^ "|" ^ Int.toString (q + 1) ^ 
   22.18 +        fun print_ln (i : int, l) = implode (Int.toString i :: "   " :: map (enclose " " " " o print_cell o (uncurry (get_descent D c))) l)
   22.19 +        val _ = tracing (implode (Int.toString (p + 1) ^ "|" ^ Int.toString (q + 1) ^ 
   22.20                                          " " :: map (enclose " " " " o Int.toString) (1 upto length callee_ms)) ^ "\n" 
   22.21                                  ^ cat_lines (map print_ln ((1 upto (length entries)) ~~ entries)))
   22.22        in
    23.1 --- a/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML	Thu Oct 15 23:10:35 2009 +0200
    23.2 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML	Thu Oct 15 23:28:10 2009 +0200
    23.3 @@ -42,7 +42,7 @@
    23.4      (case DatatypePackage.get_datatype thy ((fst o dest_Type o fastype_of) t) of
    23.5        NONE => false
    23.6      | SOME info => (let
    23.7 -      val constr_consts = flat (map (fn (_, (_, _, constrs)) => map fst constrs) (#descr info))
    23.8 +      val constr_consts = maps (fn (_, (_, _, constrs)) => map fst constrs) (#descr info)
    23.9        val (c, _) = strip_comb t
   23.10        in (case c of
   23.11          Const (name, _) => name mem_string constr_consts
   23.12 @@ -183,7 +183,7 @@
   23.13         String.isSuffix "_case" (List.last splitted_name)
   23.14      then
   23.15        (List.take (splitted_name, length splitted_name - 1)) @ ["split"]
   23.16 -      |> String.concatWith "."
   23.17 +      |> space_implode "."
   23.18        |> PureThy.get_thm thy
   23.19        |> SOME
   23.20        handle ERROR msg => NONE
    24.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Oct 15 23:10:35 2009 +0200
    24.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Oct 15 23:28:10 2009 +0200
    24.3 @@ -982,7 +982,7 @@
    24.4              val (out_ts', in_ts') = List.partition (is_constrt thy) out_ts;
    24.5              val vTs = maps term_vTs out_ts';
    24.6              val dupTs = map snd (duplicates (op =) vTs) @
    24.7 -              List.mapPartial (AList.lookup (op =) vTs) vs;
    24.8 +              map_filter (AList.lookup (op =) vTs) vs;
    24.9            in
   24.10              terms_vs (in_ts @ in_ts') subset vs andalso
   24.11              forall (is_eqT o fastype_of) in_ts' andalso
   24.12 @@ -1033,10 +1033,10 @@
   24.13    val _ = tracing ("iss:" ^
   24.14      commas (map (fn is => case is of SOME is => string_of_smode is | NONE => "NONE") iss))
   24.15      *)
   24.16 -    val modes' = modes @ List.mapPartial
   24.17 +    val modes' = modes @ map_filter
   24.18        (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
   24.19          (param_vs ~~ iss);
   24.20 -    val gen_modes' = gen_modes @ List.mapPartial
   24.21 +    val gen_modes' = gen_modes @ map_filter
   24.22        (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
   24.23          (param_vs ~~ iss);  
   24.24      val vTs = distinct (op =) ((fold o fold_prem) Term.add_frees ps (fold Term.add_frees ts []))
   24.25 @@ -1783,9 +1783,9 @@
   24.26      if (is_constructor thy t) then let
   24.27        val case_rewrites = (#case_rewrites (Datatype.the_info thy
   24.28          ((fst o dest_Type o fastype_of) t)))
   24.29 -      in case_rewrites @ (flat (map get_case_rewrite (snd (strip_comb t)))) end
   24.30 +      in case_rewrites @ maps get_case_rewrite (snd (strip_comb t)) end
   24.31      else []
   24.32 -  val simprules = @{thm "unit.cases"} :: @{thm "prod.cases"} :: (flat (map get_case_rewrite out_ts))
   24.33 +  val simprules = @{thm "unit.cases"} :: @{thm "prod.cases"} :: maps get_case_rewrite out_ts
   24.34  (* replace TRY by determining if it necessary - are there equations when calling compile match? *)
   24.35  in
   24.36     (* make this simpset better! *)
    25.1 --- a/src/HOL/Tools/TFL/casesplit.ML	Thu Oct 15 23:10:35 2009 +0200
    25.2 +++ b/src/HOL/Tools/TFL/casesplit.ML	Thu Oct 15 23:28:10 2009 +0200
    25.3 @@ -305,7 +305,7 @@
    25.4  fun derive_init_eqs sgn rules eqs =
    25.5    let
    25.6      fun get_related_thms i =
    25.7 -      List.mapPartial ((fn (r, x) => if x = i then SOME r else NONE));
    25.8 +      map_filter ((fn (r, x) => if x = i then SOME r else NONE));
    25.9      fun add_eq (i, e) xs =
   25.10        (e, (get_related_thms i rules), i) :: xs
   25.11      fun solve_eq (th, [], i) =
    26.1 --- a/src/HOL/Tools/TFL/post.ML	Thu Oct 15 23:10:35 2009 +0200
    26.2 +++ b/src/HOL/Tools/TFL/post.ML	Thu Oct 15 23:28:10 2009 +0200
    26.3 @@ -188,7 +188,7 @@
    26.4  -- Lucas Dixon, Aug 2004 *)
    26.5  local
    26.6    fun get_related_thms i = 
    26.7 -      List.mapPartial ((fn (r,x) => if x = i then SOME r else NONE));
    26.8 +      map_filter ((fn (r,x) => if x = i then SOME r else NONE));
    26.9  
   26.10    fun solve_eq (th, [], i) = 
   26.11          error "derive_init_eqs: missing rules"
   26.12 @@ -209,8 +209,7 @@
   26.13        fun countlist l = 
   26.14            (rev o snd o (Library.foldl (fn ((i,L), e) => (i + 1,(e,i) :: L)))) ((0,[]), l)
   26.15      in
   26.16 -      List.concat (map (fn (e,i) => solve_eq (e, (get_related_thms i rules), i))
   26.17 -                (countlist eqths))
   26.18 +      maps (fn (e,i) => solve_eq (e, (get_related_thms i rules), i)) (countlist eqths)
   26.19      end;
   26.20  end;
   26.21  
    27.1 --- a/src/HOL/Tools/TFL/tfl.ML	Thu Oct 15 23:10:35 2009 +0200
    27.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Thu Oct 15 23:28:10 2009 +0200
    27.3 @@ -258,7 +258,7 @@
    27.4        | SOME{case_const,constructors} =>
    27.5          let
    27.6              val case_const_name = #1(dest_Const case_const)
    27.7 -            val nrows = List.concat (map (expand constructors pty) rows)
    27.8 +            val nrows = maps (expand constructors pty) rows
    27.9              val subproblems = divide(constructors, pty, range_ty, nrows)
   27.10              val groups      = map #group subproblems
   27.11              and new_formals = map #new_formals subproblems
   27.12 @@ -272,8 +272,7 @@
   27.13              val types = map type_of (case_functions@[u]) @ [range_ty]
   27.14              val case_const' = Const(case_const_name, list_mk_type types)
   27.15              val tree = list_comb(case_const', case_functions@[u])
   27.16 -            val pat_rect1 = List.concat
   27.17 -                              (ListPair.map mk_pat (constructors', pat_rect))
   27.18 +            val pat_rect1 = flat (ListPair.map mk_pat (constructors', pat_rect))
   27.19          in (pat_rect1,tree)
   27.20          end
   27.21       end end
    28.1 --- a/src/HOL/Tools/TFL/thry.ML	Thu Oct 15 23:10:35 2009 +0200
    28.2 +++ b/src/HOL/Tools/TFL/thry.ML	Thu Oct 15 23:28:10 2009 +0200
    28.3 @@ -73,9 +73,9 @@
    28.4                  constructors = (map Const o the o Datatype.get_constrs thy) dtco};
    28.5  
    28.6  fun extract_info thy =
    28.7 - let val infos = (map snd o Symtab.dest o Datatype.get_all) thy
    28.8 + let val infos = map snd (Symtab.dest (Datatype.get_all thy))
    28.9   in {case_congs = map (mk_meta_eq o #case_cong) infos,
   28.10 -     case_rewrites = List.concat (map (map mk_meta_eq o #case_rewrites) infos)}
   28.11 +     case_rewrites = maps (map mk_meta_eq o #case_rewrites) infos}
   28.12   end;
   28.13  
   28.14  
    29.1 --- a/src/HOL/Tools/inductive.ML	Thu Oct 15 23:10:35 2009 +0200
    29.2 +++ b/src/HOL/Tools/inductive.ML	Thu Oct 15 23:28:10 2009 +0200
    29.3 @@ -329,7 +329,7 @@
    29.4        REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI'}] 1),
    29.5        REPEAT (FIRST
    29.6          [atac 1,
    29.7 -         resolve_tac (List.concat (map mk_mono monos) @ get_monos ctxt) 1,
    29.8 +         resolve_tac (maps mk_mono monos @ get_monos ctxt) 1,
    29.9           etac @{thm le_funE} 1, dtac @{thm le_boolD} 1])]));
   29.10  
   29.11  
    30.1 --- a/src/HOL/Tools/inductive_codegen.ML	Thu Oct 15 23:10:35 2009 +0200
    30.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Thu Oct 15 23:28:10 2009 +0200
    30.3 @@ -129,7 +129,7 @@
    30.4      string_of_mode ms)) modes));
    30.5  
    30.6  val term_vs = map (fst o fst o dest_Var) o OldTerm.term_vars;
    30.7 -val terms_vs = distinct (op =) o List.concat o (map term_vs);
    30.8 +val terms_vs = distinct (op =) o maps term_vs;
    30.9  
   30.10  (** collect all Vars in a term (with duplicates!) **)
   30.11  fun term_vTs tm =
   30.12 @@ -160,8 +160,8 @@
   30.13    let
   30.14      val ks = 1 upto length (binder_types (fastype_of t));
   30.15      val default = [Mode (([], ks), ks, [])];
   30.16 -    fun mk_modes name args = Option.map (List.concat o
   30.17 -      map (fn (m as (iss, is)) =>
   30.18 +    fun mk_modes name args = Option.map
   30.19 +     (maps (fn (m as (iss, is)) =>
   30.20          let
   30.21            val (args1, args2) =
   30.22              if length args < length iss then
   30.23 @@ -198,9 +198,9 @@
   30.24            let
   30.25              val (in_ts, out_ts) = get_args is 1 us;
   30.26              val (out_ts', in_ts') = List.partition (is_constrt thy) out_ts;
   30.27 -            val vTs = List.concat (map term_vTs out_ts');
   30.28 +            val vTs = maps term_vTs out_ts';
   30.29              val dupTs = map snd (duplicates (op =) vTs) @
   30.30 -              List.mapPartial (AList.lookup (op =) vTs) vs;
   30.31 +              map_filter (AList.lookup (op =) vTs) vs;
   30.32            in
   30.33              terms_vs (in_ts @ in_ts') subset vs andalso
   30.34              forall (is_eqT o fastype_of) in_ts' andalso
   30.35 @@ -215,7 +215,7 @@
   30.36  
   30.37  fun check_mode_clause thy arg_vs modes (iss, is) (ts, ps) =
   30.38    let
   30.39 -    val modes' = modes @ List.mapPartial
   30.40 +    val modes' = modes @ map_filter
   30.41        (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
   30.42          (arg_vs ~~ iss);
   30.43      fun check_mode_prems vs [] = SOME vs
   30.44 @@ -228,7 +228,7 @@
   30.45      val in_vs = terms_vs in_ts;
   30.46      val concl_vs = terms_vs ts
   30.47    in
   30.48 -    forall is_eqT (map snd (duplicates (op =) (List.concat (map term_vTs in_ts)))) andalso
   30.49 +    forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso
   30.50      forall (is_eqT o fastype_of) in_ts' andalso
   30.51      (case check_mode_prems (arg_vs union in_vs) ps of
   30.52         NONE => false
   30.53 @@ -263,7 +263,7 @@
   30.54    in mk_eqs x xs end;
   30.55  
   30.56  fun mk_tuple xs = Pretty.block (str "(" ::
   30.57 -  List.concat (separate [str ",", Pretty.brk 1] (map single xs)) @
   30.58 +  flat (separate [str ",", Pretty.brk 1] (map single xs)) @
   30.59    [str ")"]);
   30.60  
   30.61  fun mk_v ((names, vs), s) = (case AList.lookup (op =) vs s of
   30.62 @@ -286,8 +286,8 @@
   30.63    | is_exhaustive _ = false;
   30.64  
   30.65  fun compile_match nvs eq_ps out_ps success_p can_fail =
   30.66 -  let val eqs = List.concat (separate [str " andalso", Pretty.brk 1]
   30.67 -    (map single (List.concat (map (mk_eq o snd) nvs) @ eq_ps)));
   30.68 +  let val eqs = flat (separate [str " andalso", Pretty.brk 1]
   30.69 +    (map single (maps (mk_eq o snd) nvs @ eq_ps)));
   30.70    in
   30.71      Pretty.block
   30.72       ([str "(fn ", mk_tuple out_ps, str " =>", Pretty.brk 1] @
   30.73 @@ -305,7 +305,7 @@
   30.74      else mk_const_id module s gr
   30.75    in (space_implode "__"
   30.76      (mk_qual_id module id ::
   30.77 -      map (space_implode "_" o map string_of_int) (List.mapPartial I iss @ [is])), gr')
   30.78 +      map (space_implode "_" o map string_of_int) (map_filter I iss @ [is])), gr')
   30.79    end;
   30.80  
   30.81  fun mk_funcomp brack s k p = (if brack then parens else I)
   30.82 @@ -332,7 +332,7 @@
   30.83                       (invoke_codegen thy defs dep module true) args2 gr')
   30.84               in ((if brack andalso not (null ps andalso null ps') then
   30.85                 single o parens o Pretty.block else I)
   30.86 -                 (List.concat (separate [Pretty.brk 1]
   30.87 +                 (flat (separate [Pretty.brk 1]
   30.88                     ([str mode_id] :: ps @ map single ps'))), gr')
   30.89               end
   30.90             else apfst (single o mk_funcomp brack "??" (length (binder_types (fastype_of t))))
   30.91 @@ -342,7 +342,7 @@
   30.92  
   30.93  fun compile_clause thy defs dep module all_vs arg_vs modes (iss, is) (ts, ps) inp gr =
   30.94    let
   30.95 -    val modes' = modes @ List.mapPartial
   30.96 +    val modes' = modes @ map_filter
   30.97        (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
   30.98          (arg_vs ~~ iss);
   30.99  
  30.100 @@ -449,7 +449,7 @@
  30.101             (case mode of ([], []) => [str "()"] | _ => xs)) @
  30.102           [str " ="]),
  30.103          Pretty.brk 1] @
  30.104 -       List.concat (separate [str " ++", Pretty.brk 1] (map single cl_ps))), (gr', "and "))
  30.105 +       flat (separate [str " ++", Pretty.brk 1] (map single cl_ps))), (gr', "and "))
  30.106    end;
  30.107  
  30.108  fun compile_preds thy defs dep module all_vs arg_vs modes preds gr =
  30.109 @@ -458,7 +458,7 @@
  30.110        dep module prfx' all_vs arg_vs modes s cls mode gr')
  30.111          (((the o AList.lookup (op =) modes) s))) preds (gr, "fun ")
  30.112    in
  30.113 -    (space_implode "\n\n" (map string_of (List.concat prs)) ^ ";\n\n", gr')
  30.114 +    (space_implode "\n\n" (map string_of (flat prs)) ^ ";\n\n", gr')
  30.115    end;
  30.116  
  30.117  (**** processing of introduction rules ****)
  30.118 @@ -467,7 +467,7 @@
  30.119    (string * (int list option list * int list) list) list *
  30.120    (string * (int option list * int)) list;
  30.121  
  30.122 -fun lookup_modes gr dep = apfst List.concat (apsnd List.concat (ListPair.unzip
  30.123 +fun lookup_modes gr dep = apfst flat (apsnd flat (ListPair.unzip
  30.124    (map ((fn (SOME (Modes x), _, _) => x | _ => ([], [])) o get_node gr)
  30.125      (Graph.all_preds (fst gr) [dep]))));
  30.126  
  30.127 @@ -502,7 +502,7 @@
  30.128      let
  30.129        val _ $ u = Logic.strip_imp_concl (hd intrs);
  30.130        val args = List.take (snd (strip_comb u), nparms);
  30.131 -      val arg_vs = List.concat (map term_vs args);
  30.132 +      val arg_vs = maps term_vs args;
  30.133  
  30.134        fun get_nparms s = if s mem names then SOME nparms else
  30.135          Option.map #3 (get_clauses thy s);
    31.1 --- a/src/HOL/Tools/inductive_realizer.ML	Thu Oct 15 23:10:35 2009 +0200
    31.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Thu Oct 15 23:28:10 2009 +0200
    31.3 @@ -225,7 +225,7 @@
    31.4          let
    31.5            val Type ("fun", [U, _]) = T;
    31.6            val a :: names' = names
    31.7 -        in (list_abs_free (("x", U) :: List.mapPartial (fn intr =>
    31.8 +        in (list_abs_free (("x", U) :: map_filter (fn intr =>
    31.9            Option.map (pair (name_of_fn intr))
   31.10              (AList.lookup (op =) frees (name_of_fn intr))) intrs,
   31.11            list_comb (Const (a, Ts ---> T), fs) $ Free ("x", U)), names')
   31.12 @@ -300,7 +300,7 @@
   31.13        fold (fn s => AxClass.axiomatize_arity
   31.14          (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |>
   31.15          Extraction.add_typeof_eqns_i ty_eqs;
   31.16 -    val dts = List.mapPartial (fn (s, rs) => if s mem rsets then
   31.17 +    val dts = map_filter (fn (s, rs) => if s mem rsets then
   31.18        SOME (dt_of_intrs thy1' vs nparms rs) else NONE) rss;
   31.19  
   31.20      (** datatype representing computational content of inductive set **)
   31.21 @@ -332,7 +332,7 @@
   31.22        (Extraction.realizes_of thy2 vs
   31.23          (if c = Extraction.nullt then c else list_comb (c, map Var (rev
   31.24            (Term.add_vars (prop_of intr) []) \\ params'))) (prop_of intr)))
   31.25 -            (maps snd rss ~~ List.concat constrss);
   31.26 +            (maps snd rss ~~ flat constrss);
   31.27      val (rlzpreds, rlzpreds') =
   31.28        rintrs |> map (fn rintr =>
   31.29          let
   31.30 @@ -470,9 +470,8 @@
   31.31        (map (mk_realizer thy4 vs) (map (fn (((rule, rrule), rlz), c) =>
   31.32           (name_of_thm rule, rule, rrule, rlz,
   31.33              list_comb (c, map Var (rev (Term.add_vars (prop_of rule) []) \\ params'))))
   31.34 -              (List.concat (map snd rss) ~~ #intrs ind_info ~~ rintrs ~~
   31.35 -                 List.concat constrss))) thy4;
   31.36 -    val elimps = List.mapPartial (fn ((s, intrs), p) =>
   31.37 +              (maps snd rss ~~ #intrs ind_info ~~ rintrs ~~ flat constrss))) thy4;
   31.38 +    val elimps = map_filter (fn ((s, intrs), p) =>
   31.39        if s mem rsets then SOME (p, intrs) else NONE)
   31.40          (rss' ~~ (elims ~~ #elims ind_info));
   31.41      val thy6 = Library.foldl (fn (thy, p as (((((elim, _), _), _), _), _)) => thy |>
    32.1 --- a/src/HOL/Tools/metis_tools.ML	Thu Oct 15 23:10:35 2009 +0200
    32.2 +++ b/src/HOL/Tools/metis_tools.ML	Thu Oct 15 23:28:10 2009 +0200
    32.3 @@ -384,8 +384,8 @@
    32.4                    SOME _ => NONE          (*type instantiations are forbidden!*)
    32.5                  | NONE   => SOME (a,t)    (*internal Metis var?*)
    32.6          val _ = Output.debug (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
    32.7 -        val substs = List.mapPartial remove_typeinst (Metis.Subst.toList fsubst)
    32.8 -        val (vars,rawtms) = ListPair.unzip (List.mapPartial subst_translation substs)
    32.9 +        val substs = map_filter remove_typeinst (Metis.Subst.toList fsubst)
   32.10 +        val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
   32.11          val tms = infer_types ctxt rawtms;
   32.12          val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
   32.13          val substs' = ListPair.zip (vars, map ctm_of tms)
   32.14 @@ -664,7 +664,7 @@
   32.15    fun FOL_SOLVE mode ctxt cls ths0 =
   32.16      let val thy = ProofContext.theory_of ctxt
   32.17          val th_cls_pairs = map (fn th => (Thm.get_name_hint th, ResAxioms.cnf_axiom thy th)) ths0
   32.18 -        val ths = List.concat (map #2 th_cls_pairs)
   32.19 +        val ths = maps #2 th_cls_pairs
   32.20          val _ = Output.debug (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
   32.21          val _ = app (fn th => Output.debug (fn () => Display.string_of_thm ctxt th)) cls
   32.22          val _ = Output.debug (fn () => "THEOREM CLAUSES")
   32.23 @@ -690,7 +690,7 @@
   32.24                                 (*add constraints arising from converting goal to clause form*)
   32.25                    val proof = Metis.Proof.proof mth
   32.26                    val result = translate mode ctxt' axioms proof
   32.27 -                  and used = List.mapPartial (used_axioms axioms) proof
   32.28 +                  and used = map_filter (used_axioms axioms) proof
   32.29                    val _ = Output.debug (fn () => "METIS COMPLETED...clauses actually used:")
   32.30  	          val _ = app (fn th => Output.debug (fn () => Display.string_of_thm ctxt th)) used
   32.31  	          val unused = filter (fn (a,cls) => not (common_thm used cls)) th_cls_pairs
    33.1 --- a/src/HOL/Tools/recdef.ML	Thu Oct 15 23:10:35 2009 +0200
    33.2 +++ b/src/HOL/Tools/recdef.ML	Thu Oct 15 23:28:10 2009 +0200
    33.3 @@ -209,7 +209,7 @@
    33.4        thy
    33.5        |> Sign.add_path bname
    33.6        |> PureThy.add_thmss
    33.7 -        (((Binding.name "simps", List.concat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
    33.8 +        (((Binding.name "simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
    33.9        ||>> PureThy.add_thms [((Binding.name "induct", induct), [])];
   33.10      val result = {simps = simps', rules = rules', induct = induct', tcs = tcs};
   33.11      val thy =
    34.1 --- a/src/HOL/Tools/recfun_codegen.ML	Thu Oct 15 23:10:35 2009 +0200
    34.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Thu Oct 15 23:28:10 2009 +0200
    34.3 @@ -119,7 +119,7 @@
    34.4                 let
    34.5                   val thmss as (_, thyname) :: _ = map (get_equations thy defs) cs;
    34.6                   val module' = if_library thyname module;
    34.7 -                 val eqs'' = map (dest_eq o prop_of) (List.concat (map fst thmss));
    34.8 +                 val eqs'' = map (dest_eq o prop_of) (maps fst thmss);
    34.9                   val (fundef', gr3) = mk_fundef module' "" true eqs''
   34.10                     (add_edge (dname, dep)
   34.11                       (List.foldr (uncurry new_node) (del_nodes xs gr2)
    35.1 --- a/src/HOL/Tools/record.ML	Thu Oct 15 23:10:35 2009 +0200
    35.2 +++ b/src/HOL/Tools/record.ML	Thu Oct 15 23:28:10 2009 +0200
    35.3 @@ -656,7 +656,7 @@
    35.4  
    35.5          fun bad_inst ((x, S), T) =
    35.6            if Sign.of_sort thy (T, S) then NONE else SOME x
    35.7 -        val bads = List.mapPartial bad_inst (args ~~ types);
    35.8 +        val bads = map_filter bad_inst (args ~~ types);
    35.9          val _ = null bads orelse err ("Ill-sorted instantiation of " ^ commas bads ^ " in");
   35.10  
   35.11          val inst = map fst args ~~ types;
   35.12 @@ -1362,7 +1362,7 @@
   35.13            | mk_updterm us _ _ = raise TERM ("mk_updterm match", map (fn (x, _, _) => x) us);
   35.14  
   35.15          val (lhs, rhs, vars, _, simp, noops) = mk_updterm upds Symtab.empty base;
   35.16 -        val noops' = flat (map snd (Symtab.dest noops));
   35.17 +        val noops' = maps snd (Symtab.dest noops);
   35.18        in
   35.19          if simp then
   35.20            SOME
   35.21 @@ -1521,7 +1521,7 @@
   35.22                end)
   35.23        | split_free_tac _ _ _ = NONE;
   35.24  
   35.25 -    val split_frees_tacs = List.mapPartial (split_free_tac P i) frees;
   35.26 +    val split_frees_tacs = map_filter (split_free_tac P i) frees;
   35.27  
   35.28      val simprocs = if has_rec goal then [record_split_simproc P] else [];
   35.29      val thms' = K_comp_convs @ thms;
   35.30 @@ -1860,7 +1860,7 @@
   35.31      val (bfields, field_syntax) =
   35.32        split_list (map (fn (x, T, mx) => ((x, T), mx)) raw_fields);
   35.33  
   35.34 -    val parent_fields = List.concat (map #fields parents);
   35.35 +    val parent_fields = maps #fields parents;
   35.36      val parent_chunks = map (length o #fields) parents;
   35.37      val parent_names = map fst parent_fields;
   35.38      val parent_types = map snd parent_fields;
    36.1 --- a/src/HOL/Tools/refute.ML	Thu Oct 15 23:10:35 2009 +0200
    36.2 +++ b/src/HOL/Tools/refute.ML	Thu Oct 15 23:28:10 2009 +0200
    36.3 @@ -281,7 +281,7 @@
    36.4        if null terms then
    36.5          "empty interpretation (no free variables in term)\n"
    36.6        else
    36.7 -        cat_lines (List.mapPartial (fn (t, intr) =>
    36.8 +        cat_lines (map_filter (fn (t, intr) =>
    36.9            (* print constants only if 'show_consts' is true *)
   36.10            if (!show_consts) orelse not (is_Const t) then
   36.11              SOME (Syntax.string_of_term_global thy t ^ ": " ^
   36.12 @@ -395,7 +395,7 @@
   36.13      (* TODO: it is currently not possible to specify a size for a type    *)
   36.14      (*       whose name is one of the other parameters (e.g. 'maxvars')   *)
   36.15      (* (string * int) list *)
   36.16 -    val sizes     = List.mapPartial
   36.17 +    val sizes     = map_filter
   36.18        (fn (name, value) => Option.map (pair name) (Int.fromString value))
   36.19        (List.filter (fn (name, _) => name<>"minsize" andalso name<>"maxsize"
   36.20          andalso name<>"maxvars" andalso name<>"maxtime"
   36.21 @@ -994,8 +994,7 @@
   36.22                      (* collect argument types *)
   36.23                      val acc_dtyps = List.foldr collect_dtyp acc_dT dtyps
   36.24                      (* collect constructor types *)
   36.25 -                    val acc_dconstrs = List.foldr collect_dtyp acc_dtyps
   36.26 -                      (List.concat (map snd dconstrs))
   36.27 +                    val acc_dconstrs = List.foldr collect_dtyp acc_dtyps (maps snd dconstrs)
   36.28                    in
   36.29                      acc_dconstrs
   36.30                    end
   36.31 @@ -1389,7 +1388,7 @@
   36.32        map single xs
   36.33        | pick_all n xs =
   36.34        let val rec_pick = pick_all (n-1) xs in
   36.35 -        List.concat (map (fn x => map (cons x) rec_pick) xs)
   36.36 +        maps (fn x => map (cons x) rec_pick) xs
   36.37        end
   36.38      (* returns all constant interpretations that have the same tree *)
   36.39      (* structure as the interpretation argument                     *)
   36.40 @@ -1582,7 +1581,7 @@
   36.41        map single xs
   36.42        | pick_all (xs::xss) =
   36.43        let val rec_pick = pick_all xss in
   36.44 -        List.concat (map (fn x => map (cons x) rec_pick) xs)
   36.45 +        maps (fn x => map (cons x) rec_pick) xs
   36.46        end
   36.47        | pick_all _ =
   36.48        raise REFUTE ("interpretation_apply", "empty list (in pick_all)")
   36.49 @@ -2068,7 +2067,7 @@
   36.50              map single xs
   36.51            | pick_all n xs =
   36.52              let val rec_pick = pick_all (n-1) xs in
   36.53 -              List.concat (map (fn x => map (cons x) rec_pick) xs)
   36.54 +              maps (fn x => map (cons x) rec_pick) xs
   36.55              end
   36.56            (* ["x1", ..., "xn"] *)
   36.57            val terms1 = canonical_terms typs T1
   36.58 @@ -2131,13 +2130,13 @@
   36.59                  end
   36.60              in
   36.61                (* C_i ... < C_j ... if i < j *)
   36.62 -              List.concat (map (fn (cname, ctyps) =>
   36.63 +              maps (fn (cname, ctyps) =>
   36.64                  let
   36.65                    val cTerm = Const (cname,
   36.66                      map (typ_of_dtyp descr typ_assoc) ctyps ---> T)
   36.67                  in
   36.68                    constructor_terms [cTerm] ctyps
   36.69 -                end) constrs)
   36.70 +                end) constrs
   36.71              end)
   36.72          | NONE =>
   36.73            (* not an inductive datatype; in this case the argument types in *)
   36.74 @@ -2483,14 +2482,14 @@
   36.75                      (* of the parameter must be ignored                     *)
   36.76                      if List.exists (equal True) xs then [pi] else []
   36.77                      | ci_pi (Node xs, Node ys) =
   36.78 -                    List.concat (map ci_pi (xs ~~ ys))
   36.79 +                    maps ci_pi (xs ~~ ys)
   36.80                      | ci_pi (Node _, Leaf _) =
   36.81                      raise REFUTE ("IDT_recursion_interpreter",
   36.82                        "constructor takes more arguments than the " ^
   36.83                          "associated parameter")
   36.84                    (* (int * interpretation list) list *)
   36.85                    val rec_operators = map (fn (idx, c_p_intrs) =>
   36.86 -                    (idx, List.concat (map ci_pi c_p_intrs))) mc_p_intrs
   36.87 +                    (idx, maps ci_pi c_p_intrs)) mc_p_intrs
   36.88                    (* sanity check: every recursion operator must provide as  *)
   36.89                    (*               many values as the corresponding datatype *)
   36.90                    (*               has elements                              *)
   36.91 @@ -3080,8 +3079,7 @@
   36.92          val constants_T = make_constants thy model T
   36.93          val size_U      = size_of_type thy model U
   36.94        in
   36.95 -        SOME (Node (List.concat (map (replicate size_U) constants_T)),
   36.96 -          model, args)
   36.97 +        SOME (Node (maps (replicate size_U) constants_T), model, args)
   36.98        end
   36.99      | _ =>
  36.100        NONE;
  36.101 @@ -3100,7 +3098,7 @@
  36.102          val size_T      = size_of_type thy model T
  36.103          val constants_U = make_constants thy model U
  36.104        in
  36.105 -        SOME (Node (List.concat (replicate size_T constants_U)), model, args)
  36.106 +        SOME (Node (flat (replicate size_T constants_U)), model, args)
  36.107        end
  36.108      | _ =>
  36.109        NONE;
    37.1 --- a/src/HOL/Tools/res_atp.ML	Thu Oct 15 23:10:35 2009 +0200
    37.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Oct 15 23:28:10 2009 +0200
    37.3 @@ -251,7 +251,7 @@
    37.4    let fun relevant ([],_) [] = [] : (thm * (string * int)) list  (*Nothing added this iteration*)
    37.5  	| relevant (newpairs,rejects) [] =
    37.6  	    let val (newrels,more_rejects) = take_best max_new newpairs
    37.7 -		val new_consts = List.concat (map #2 newrels)
    37.8 +		val new_consts = maps #2 newrels
    37.9  		val rel_consts' = List.foldl add_const_typ_table rel_consts new_consts
   37.10  		val newp = p + (1.0-p) / convergence
   37.11  	    in
   37.12 @@ -425,7 +425,7 @@
   37.13  (* Type Classes Present in the Axiom or Conjecture Clauses     *)
   37.14  (***************************************************************)
   37.15  
   37.16 -fun add_classes (sorts, cset) = List.foldl setinsert cset (List.concat sorts);
   37.17 +fun add_classes (sorts, cset) = List.foldl setinsert cset (flat sorts);
   37.18  
   37.19  (*Remove this trivial type class*)
   37.20  fun delete_type cset = Symtab.delete_safe "HOL.type" cset;
    38.1 --- a/src/HOL/Tools/res_reconstruct.ML	Thu Oct 15 23:10:35 2009 +0200
    38.2 +++ b/src/HOL/Tools/res_reconstruct.ML	Thu Oct 15 23:28:10 2009 +0200
    38.3 @@ -422,7 +422,7 @@
    38.4                 fun fix lno = if lno <= Vector.length thm_names
    38.5                               then SOME(Vector.sub(thm_names,lno-1))
    38.6                               else AList.lookup op= deps_map lno;
    38.7 -           in  (lname, t, List.mapPartial fix (distinct (op=) deps)) ::
    38.8 +           in  (lname, t, map_filter fix (distinct (op=) deps)) ::
    38.9                 stringify_deps thm_names ((lno,lname)::deps_map) lines
   38.10             end;
   38.11  
   38.12 @@ -451,7 +451,7 @@
   38.13        val ilines = isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines)
   38.14        val _ = trace "\ndecode_tstp_file: finishing\n"
   38.15    in
   38.16 -    isar_header (map #1 fixes) ^ String.concat ilines ^ "qed\n"
   38.17 +    isar_header (map #1 fixes) ^ implode ilines ^ "qed\n"
   38.18    end;
   38.19  
   38.20  
   38.21 @@ -504,7 +504,7 @@
   38.22        | inputno ("cnf"::ntok::"negated"::"conjecture"::_) = Int.fromString ntok
   38.23        | inputno _ = NONE
   38.24      val lines = split_lines proofextract
   38.25 -    in  List.mapPartial (inputno o toks) lines  end
   38.26 +    in  map_filter (inputno o toks) lines  end
   38.27    (*String contains multiple lines. We want those of the form
   38.28      "253[0:Inp] et cetera..."
   38.29      A list consisting of the first number in each line is returned. *)
   38.30 @@ -513,7 +513,7 @@
   38.31      fun inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok
   38.32        | inputno _ = NONE
   38.33      val lines = split_lines proofextract
   38.34 -    in  List.mapPartial (inputno o toks) lines  end
   38.35 +    in  map_filter (inputno o toks) lines  end
   38.36      
   38.37    (*extracting lemmas from tstp-output between the lines from above*)
   38.38    fun extract_lemmas get_step_nums (proof, thm_names, conj_count, _, _, _) =
    39.1 --- a/src/HOL/Tools/sat_solver.ML	Thu Oct 15 23:10:35 2009 +0200
    39.2 +++ b/src/HOL/Tools/sat_solver.ML	Thu Oct 15 23:28:10 2009 +0200
    39.3 @@ -233,7 +233,7 @@
    39.4    let
    39.5      (* string -> int list *)
    39.6      fun int_list_from_string s =
    39.7 -      List.mapPartial Int.fromString (space_explode " " s)
    39.8 +      map_filter Int.fromString (space_explode " " s)
    39.9      (* int list -> assignment *)
   39.10      fun assignment_from_list [] i =
   39.11        NONE  (* the SAT solver didn't provide a value for this variable *)
   39.12 @@ -350,8 +350,7 @@
   39.13      o (map (map literal_from_int))
   39.14      o clauses
   39.15      o (map int_from_string)
   39.16 -    o List.concat
   39.17 -    o (map (String.fields (fn c => c mem [#" ", #"\t", #"\n"])))
   39.18 +    o (maps (String.fields (fn c => c mem [#" ", #"\t", #"\n"])))
   39.19      o filter_preamble
   39.20      o (List.filter (fn l => l <> ""))
   39.21      o split_lines
    40.1 --- a/src/HOL/ex/predicate_compile.ML	Thu Oct 15 23:10:35 2009 +0200
    40.2 +++ b/src/HOL/ex/predicate_compile.ML	Thu Oct 15 23:28:10 2009 +0200
    40.3 @@ -906,7 +906,7 @@
    40.4              val (out_ts', in_ts') = List.partition (is_constrt thy) out_ts;
    40.5              val vTs = maps term_vTs out_ts';
    40.6              val dupTs = map snd (duplicates (op =) vTs) @
    40.7 -              List.mapPartial (AList.lookup (op =) vTs) vs;
    40.8 +              map_filter (AList.lookup (op =) vTs) vs;
    40.9            in
   40.10              terms_vs (in_ts @ in_ts') subset vs andalso
   40.11              forall (is_eqT o fastype_of) in_ts' andalso
   40.12 @@ -950,10 +950,10 @@
   40.13    
   40.14  fun check_mode_clause with_generator thy param_vs modes gen_modes (iss, is) (ts, ps) =
   40.15    let
   40.16 -    val modes' = modes @ List.mapPartial
   40.17 +    val modes' = modes @ map_filter
   40.18        (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
   40.19          (param_vs ~~ iss);
   40.20 -    val gen_modes' = gen_modes @ List.mapPartial
   40.21 +    val gen_modes' = gen_modes @ map_filter
   40.22        (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
   40.23          (param_vs ~~ iss);  
   40.24      val vTs = distinct (op =) ((fold o fold_prem) Term.add_frees ps (fold Term.add_frees ts []))
   40.25 @@ -1547,9 +1547,9 @@
   40.26      if (is_constructor thy t) then let
   40.27        val case_rewrites = (#case_rewrites (Datatype.the_info thy
   40.28          ((fst o dest_Type o fastype_of) t)))
   40.29 -      in case_rewrites @ (flat (map get_case_rewrite (snd (strip_comb t)))) end
   40.30 +      in case_rewrites @ maps get_case_rewrite (snd (strip_comb t)) end
   40.31      else []
   40.32 -  val simprules = @{thm "unit.cases"} :: @{thm "prod.cases"} :: (flat (map get_case_rewrite out_ts))
   40.33 +  val simprules = @{thm "unit.cases"} :: @{thm "prod.cases"} :: maps get_case_rewrite out_ts
   40.34  (* replace TRY by determining if it necessary - are there equations when calling compile match? *)
   40.35  in
   40.36     (* make this simpset better! *)
    41.1 --- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Thu Oct 15 23:10:35 2009 +0200
    41.2 +++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Thu Oct 15 23:28:10 2009 +0200
    41.3 @@ -123,7 +123,7 @@
    41.4                                                                list_ccomb(%%:(dname^"_when"),map 
    41.5                                                                                                (fn (con',args) => if con'<>con then UU else
    41.6                                                                                                                   List.foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg);
    41.7 -      in List.mapPartial I (List.concat(map (fn (con,args) => mapn (sdef con) 1 args) cons)) end;
    41.8 +      in map_filter I (maps (fn (con,args) => mapn (sdef con) 1 args) cons) end;
    41.9  
   41.10  
   41.11        (* ----- axiom and definitions concerning induction ------------------------- *)
    42.1 --- a/src/HOLCF/Tools/Domain/domain_extender.ML	Thu Oct 15 23:10:35 2009 +0200
    42.2 +++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Thu Oct 15 23:28:10 2009 +0200
    42.3 @@ -33,12 +33,12 @@
    42.4        val test_dupl_typs = (case duplicates (op =) (map fst dtnvs) of 
    42.5                                [] => false | dups => error ("Duplicate types: " ^ commas_quote dups));
    42.6        val test_dupl_cons =
    42.7 -          (case duplicates (op =) (map (Binding.name_of o first) (List.concat cons'')) of 
    42.8 +          (case duplicates (op =) (map (Binding.name_of o first) (flat cons'')) of 
    42.9               [] => false | dups => error ("Duplicate constructors: " 
   42.10                                            ^ commas_quote dups));
   42.11        val test_dupl_sels =
   42.12 -          (case duplicates (op =) (map Binding.name_of (List.mapPartial second
   42.13 -                                                                        (List.concat (map second (List.concat cons''))))) of
   42.14 +          (case duplicates (op =) (map Binding.name_of (map_filter second
   42.15 +                                                                        (maps second (flat cons'')))) of
   42.16               [] => false | dups => error("Duplicate selectors: "^commas_quote dups));
   42.17        val test_dupl_tvars =
   42.18            exists(fn s=>case duplicates (op =) (map(fst o dest_TFree)s)of
   42.19 @@ -142,7 +142,7 @@
   42.20      in
   42.21        theorems_thy
   42.22          |> Sign.add_path (Long_Name.base_name comp_dnam)
   42.23 -        |> (snd o (PureThy.add_thmss [((Binding.name "rews", List.concat rewss @ take_rews), [])]))
   42.24 +        |> (snd o (PureThy.add_thmss [((Binding.name "rews", flat rewss @ take_rews), [])]))
   42.25          |> Sign.parent_path
   42.26      end;
   42.27  
    43.1 --- a/src/HOLCF/Tools/Domain/domain_syntax.ML	Thu Oct 15 23:10:35 2009 +0200
    43.2 +++ b/src/HOLCF/Tools/Domain/domain_syntax.ML	Thu Oct 15 23:28:10 2009 +0200
    43.3 @@ -76,7 +76,7 @@
    43.4                                   mk_matT(dtype, map third args, freetvar "t" 1),
    43.5                                   Mixfix(escape ("match_" ^ Binding.name_of con), [], Syntax.max_pri));
    43.6          fun sel1 (_,sel,typ)  = Option.map (fn s => (s,dtype ->> typ,NoSyn)) sel;
    43.7 -        fun sel (con,args,mx) = List.mapPartial sel1 args;
    43.8 +        fun sel (con,args,mx) = map_filter sel1 args;
    43.9          fun mk_patT (a,b)     = a ->> mk_maybeT b;
   43.10          fun pat_arg_typ n arg = mk_patT (third arg, freetvar "t" n);
   43.11          fun pat (con,args,mx) = (pat_name_ con,
   43.12 @@ -90,7 +90,7 @@
   43.13        val consts_dis = map dis cons';
   43.14        val consts_mat = map mat cons';
   43.15        val consts_pat = map pat cons';
   43.16 -      val consts_sel = List.concat(map sel cons');
   43.17 +      val consts_sel = maps sel cons';
   43.18        end;
   43.19  
   43.20        (* ----- constants concerning induction ------------------------------------- *)
   43.21 @@ -147,7 +147,7 @@
   43.22               PrintRule (Library.foldl capp (cname, ListPair.map (app "_match") (ps,vs)),
   43.23                          app "_match" (mk_appl pname ps, args_list vs))]
   43.24            end;
   43.25 -      val Case_trans = List.concat (map one_case_trans cons');
   43.26 +      val Case_trans = maps one_case_trans cons';
   43.27        end;
   43.28        end;
   43.29  
   43.30 @@ -172,10 +172,10 @@
   43.31        val const_copy = (Binding.name (comp_dnam^"_copy"), funprod ->> funprod, NoSyn);
   43.32        val const_bisim = (Binding.name (comp_dnam^"_bisim"), relprod --> boolT, NoSyn);
   43.33        val ctt : ((binding * typ * mixfix) list * ast Syntax.trrule list) list = map (calc_syntax funprod) eqs';
   43.34 -    in thy'' |> ContConsts.add_consts_i (List.concat (map fst ctt) @ 
   43.35 +    in thy'' |> ContConsts.add_consts_i (maps fst ctt @ 
   43.36                                           (if length eqs'>1 then [const_copy] else[])@
   43.37                                           [const_bisim])
   43.38 -             |> Sign.add_trrules_i (List.concat(map snd ctt))
   43.39 +             |> Sign.add_trrules_i (maps snd ctt)
   43.40      end; (* let *)
   43.41  
   43.42  end; (* struct *)
    44.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Oct 15 23:10:35 2009 +0200
    44.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Oct 15 23:28:10 2009 +0200
    44.3 @@ -149,7 +149,7 @@
    44.4      let
    44.5        fun def_of_sel sel = ga (sel^"_def") dname;
    44.6        fun def_of_arg arg = Option.map def_of_sel (sel_of arg);
    44.7 -      fun defs_of_con (_, args) = List.mapPartial def_of_arg args;
    44.8 +      fun defs_of_con (_, args) = map_filter def_of_arg args;
    44.9      in
   44.10        maps defs_of_con cons
   44.11      end;
   44.12 @@ -434,7 +434,7 @@
   44.13        (K [simp_tac (HOLCF_ss addsimps when_rews) 1]);
   44.14  
   44.15    fun sel_strict (_, args) =
   44.16 -    List.mapPartial (Option.map one_sel o sel_of) args;
   44.17 +    map_filter (Option.map one_sel o sel_of) args;
   44.18  in
   44.19    val _ = trace " Proving sel_stricts...";
   44.20    val sel_stricts = maps sel_strict cons;
   44.21 @@ -492,7 +492,7 @@
   44.22    val _ = trace " Proving sel_defins...";
   44.23    val sel_defins =
   44.24      if length cons = 1
   44.25 -    then List.mapPartial (fn arg => Option.map sel_defin (sel_of arg))
   44.26 +    then map_filter (fn arg => Option.map sel_defin (sel_of arg))
   44.27                   (filter_out is_lazy (snd (hd cons)))
   44.28      else [];
   44.29  end;
    45.1 --- a/src/HOLCF/Tools/fixrec.ML	Thu Oct 15 23:10:35 2009 +0200
    45.2 +++ b/src/HOLCF/Tools/fixrec.ML	Thu Oct 15 23:28:10 2009 +0200
    45.3 @@ -371,7 +371,7 @@
    45.4        val simps1 : (Attrib.binding * thm list) list =
    45.5          map (fn (n,xs) => (mk_bind n, map snd xs)) (names ~~ simps);
    45.6        val simps2 : (Attrib.binding * thm list) list =
    45.7 -        map (apsnd (fn thm => [thm])) (List.concat simps);
    45.8 +        map (apsnd (fn thm => [thm])) (flat simps);
    45.9        val (_, lthy'') = lthy'
   45.10          |> fold_map (LocalTheory.note Thm.generatedK) (simps1 @ simps2);
   45.11      in
    46.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Thu Oct 15 23:10:35 2009 +0200
    46.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Thu Oct 15 23:28:10 2009 +0200
    46.3 @@ -720,7 +720,7 @@
    46.4              val mkleq = mklineq n atoms
    46.5              val ixs = 0 upto (n - 1)
    46.6              val iatoms = atoms ~~ ixs
    46.7 -            val natlineqs = List.mapPartial (mknat Ts ixs) iatoms
    46.8 +            val natlineqs = map_filter (mknat Ts ixs) iatoms
    46.9              val ineqs = map mkleq initems @ natlineqs
   46.10            in case elim (ineqs, []) of
   46.11                 Success j =>
    47.1 --- a/src/Provers/classical.ML	Thu Oct 15 23:10:35 2009 +0200
    47.2 +++ b/src/Provers/classical.ML	Thu Oct 15 23:28:10 2009 +0200
    47.3 @@ -938,7 +938,7 @@
    47.4      val ruleq = Drule.multi_resolves facts rules;
    47.5    in
    47.6      Method.trace ctxt rules;
    47.7 -    fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq)
    47.8 +    fn st => Seq.maps (fn rule => Tactic.rtac rule i st) ruleq
    47.9    end)
   47.10    THEN_ALL_NEW Goal.norm_hhf_tac;
   47.11  
    48.1 --- a/src/Provers/order.ML	Thu Oct 15 23:10:35 2009 +0200
    48.2 +++ b/src/Provers/order.ML	Thu Oct 15 23:28:10 2009 +0200
    48.3 @@ -735,7 +735,7 @@
    48.4      ListPair.map (fn (a,b) => (a,b)) (0 upto (length components -1), components);
    48.5  
    48.6  fun indexNodes IndexComp =
    48.7 -    List.concat (map (fn (index, comp) => (map (fn v => (v,index)) comp)) IndexComp);
    48.8 +    maps (fn (index, comp) => (map (fn v => (v,index)) comp)) IndexComp;
    48.9  
   48.10  fun getIndex v [] = ~1
   48.11  |   getIndex v ((v',k)::vs) = if v aconv v' then k else getIndex v vs;
   48.12 @@ -1142,9 +1142,9 @@
   48.13      fun processComponent (k, comp) =
   48.14       let
   48.15          (* all edges with weight <= of the actual component *)
   48.16 -        val leqEdges = List.concat (map (adjacent (op aconv) leqG) comp);
   48.17 +        val leqEdges = maps (adjacent (op aconv) leqG) comp;
   48.18          (* all edges with weight ~= of the actual component *)
   48.19 -        val neqEdges = map snd (List.concat (map (adjacent (op aconv) neqG) comp));
   48.20 +        val neqEdges = map snd (maps (adjacent (op aconv) neqG) comp);
   48.21  
   48.22         (* find an edge leading to a contradiction *)
   48.23         fun findContr [] = NONE
   48.24 @@ -1231,7 +1231,7 @@
   48.25     val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A));
   48.26     val Hs = map prop_of prems @ map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
   48.27     val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
   48.28 -   val lesss = List.concat (ListPair.map (mkasm decomp less_thms thy) (Hs, 0 upto (length Hs - 1)))
   48.29 +   val lesss = flat (ListPair.map (mkasm decomp less_thms thy) (Hs, 0 upto (length Hs - 1)))
   48.30     val prfs = gen_solve mkconcl thy (lesss, C);
   48.31     val (subgoals, prf) = mkconcl decomp less_thms thy C;
   48.32    in
    49.1 --- a/src/Provers/quasi.ML	Thu Oct 15 23:10:35 2009 +0200
    49.2 +++ b/src/Provers/quasi.ML	Thu Oct 15 23:28:10 2009 +0200
    49.3 @@ -555,7 +555,7 @@
    49.4    val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A));
    49.5    val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A);
    49.6    val C = subst_bounds (rfrees, Logic.strip_assums_concl A);
    49.7 -  val lesss = List.concat (ListPair.map (mkasm_trans thy) (Hs, 0 upto (length Hs - 1)));
    49.8 +  val lesss = flat (ListPair.map (mkasm_trans thy) (Hs, 0 upto (length Hs - 1)));
    49.9    val prfs = solveLeTrans thy (lesss, C);
   49.10  
   49.11    val (subgoal, prf) = mkconcl_trans thy C;
    50.1 --- a/src/Pure/codegen.ML	Thu Oct 15 23:10:35 2009 +0200
    50.2 +++ b/src/Pure/codegen.ML	Thu Oct 15 23:28:10 2009 +0200
    50.3 @@ -742,8 +742,7 @@
    50.4  
    50.5  fun mk_tuple [p] = p
    50.6    | mk_tuple ps = Pretty.block (str "(" ::
    50.7 -      List.concat (separate [str ",", Pretty.brk 1] (map single ps)) @
    50.8 -        [str ")"]);
    50.9 +      flat (separate [str ",", Pretty.brk 1] (map single ps)) @ [str ")"]);
   50.10  
   50.11  fun mk_let bindings body =
   50.12    Pretty.blk (0, [str "let", Pretty.brk 1,
    51.1 --- a/src/Tools/Compute_Oracle/am_ghc.ML	Thu Oct 15 23:10:35 2009 +0200
    51.2 +++ b/src/Tools/Compute_Oracle/am_ghc.ML	Thu Oct 15 23:28:10 2009 +0200
    51.3 @@ -84,7 +84,7 @@
    51.4  	     in
    51.5  		 if a <= len then 
    51.6  		     let
    51.7 -			 val s = "c"^(str c)^(concat (map (fn t => " "^(protect_blank (print_term d t))) (List.take (args, a))))
    51.8 +			 val s = "c"^(str c)^(implode (map (fn t => " "^(protect_blank (print_term d t))) (List.take (args, a))))
    51.9  		     in
   51.10  			 print_apps d s (List.drop (args, a))
   51.11  		     end
   51.12 @@ -154,19 +154,19 @@
   51.13  	val rules = group_rules rules
   51.14  	val constants = Inttab.keys arity
   51.15  	fun arity_of c = Inttab.lookup arity c
   51.16 -	fun rep_str s n = concat (rep n s)
   51.17 +	fun rep_str s n = implode (rep n s)
   51.18  	fun indexed s n = s^(str n)
   51.19  	fun section n = if n = 0 then [] else (section (n-1))@[n-1]
   51.20  	fun make_show c = 
   51.21  	    let
   51.22  		val args = section (the (arity_of c))
   51.23  	    in
   51.24 -		"  show ("^(indexed "C" c)^(concat (map (indexed " a") args))^") = "
   51.25 -		^"\""^(indexed "C" c)^"\""^(concat (map (fn a => "++(show "^(indexed "a" a)^")") args))
   51.26 +		"  show ("^(indexed "C" c)^(implode (map (indexed " a") args))^") = "
   51.27 +		^"\""^(indexed "C" c)^"\""^(implode (map (fn a => "++(show "^(indexed "a" a)^")") args))
   51.28  	    end
   51.29  	fun default_case c = 
   51.30  	    let
   51.31 -		val args = concat (map (indexed " x") (section (the (arity_of c))))
   51.32 +		val args = implode (map (indexed " x") (section (the (arity_of c))))
   51.33  	    in
   51.34  		(indexed "c" c)^args^" = "^(indexed "C" c)^args
   51.35  	    end
   51.36 @@ -174,7 +174,7 @@
   51.37  		"module "^name^" where",
   51.38  		"",
   51.39  		"data Term = Const Integer | App Term Term | Abs (Term -> Term)",
   51.40 -		"         "^(concat (map (fn c => " | C"^(str c)^(rep_str " Term" (the (arity_of c)))) constants)),
   51.41 +		"         "^(implode (map (fn c => " | C"^(str c)^(rep_str " Term" (the (arity_of c)))) constants)),
   51.42  		"",
   51.43  		"instance Show Term where"]
   51.44  	val _ = writelist (map make_show constants)
    52.1 --- a/src/Tools/Compute_Oracle/am_sml.ML	Thu Oct 15 23:10:35 2009 +0200
    52.2 +++ b/src/Tools/Compute_Oracle/am_sml.ML	Thu Oct 15 23:28:10 2009 +0200
    52.3 @@ -206,8 +206,8 @@
    52.4  		     let
    52.5  			 val strict_a = (case toplevel_arity_of c of SOME sa => sa | NONE => a)
    52.6  			 val _ = if strict_a > a then raise Compile "strict" else ()
    52.7 -			 val s = module_prefix^"c"^(str c)^(concat (map (fn t => " "^(protect_blank (print_term d t))) (List.take (args, strict_a))))
    52.8 -			 val s = s^(concat (map (fn t => " (fn () => "^print_term d t^")") (List.drop (List.take (args, a), strict_a))))
    52.9 +			 val s = module_prefix^"c"^(str c)^(implode (map (fn t => " "^(protect_blank (print_term d t))) (List.take (args, strict_a))))
   52.10 +			 val s = s^(implode (map (fn t => " (fn () => "^print_term d t^")") (List.drop (List.take (args, a), strict_a))))
   52.11  		     in
   52.12  			 print_apps d s (List.drop (args, a))
   52.13  		     end
   52.14 @@ -273,9 +273,9 @@
   52.15  	val lazy_vars = the (arity_of c) - the (toplevel_arity_of c)
   52.16  	fun print_tm tm = print_term NONE arity_of toplevel_arity_of n lazy_vars tm
   52.17          fun print_guard (Guard (a,b)) = "term_eq ("^(print_tm a)^") ("^(print_tm b)^")"
   52.18 -	val else_branch = "c"^(str c)^"_"^(str (gnum+1))^(concat (map (fn i => " a"^(str i)) (section (the (arity_of c)))))
   52.19 +	val else_branch = "c"^(str c)^"_"^(str (gnum+1))^(implode (map (fn i => " a"^(str i)) (section (the (arity_of c)))))
   52.20  	fun print_guards t [] = print_tm t
   52.21 -	  | 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
   52.22 +	  | 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
   52.23      in
   52.24  	(if null guards then gnum else gnum+1, pattern^" = "^(print_guards t guards))
   52.25      end
   52.26 @@ -307,15 +307,15 @@
   52.27  	val constants = Inttab.keys arity
   52.28  	fun arity_of c = Inttab.lookup arity c
   52.29  	fun toplevel_arity_of c = Inttab.lookup toplevel_arity c
   52.30 -	fun rep_str s n = concat (rep n s)
   52.31 +	fun rep_str s n = implode (rep n s)
   52.32  	fun indexed s n = s^(str n)
   52.33          fun string_of_tuple [] = ""
   52.34 -	  | string_of_tuple (x::xs) = "("^x^(concat (map (fn s => ", "^s) xs))^")"
   52.35 +	  | string_of_tuple (x::xs) = "("^x^(implode (map (fn s => ", "^s) xs))^")"
   52.36          fun string_of_args [] = ""
   52.37 -	  | string_of_args (x::xs) = x^(concat (map (fn s => " "^s) xs))
   52.38 +	  | string_of_args (x::xs) = x^(implode (map (fn s => " "^s) xs))
   52.39  	fun default_case gnum c = 
   52.40  	    let
   52.41 -		val leftargs = concat (map (indexed " x") (section (the (arity_of c))))
   52.42 +		val leftargs = implode (map (indexed " x") (section (the (arity_of c))))
   52.43  		val rightargs = section (the (arity_of c))
   52.44  		val strict_args = (case toplevel_arity_of c of NONE => the (arity_of c) | SOME sa => sa)
   52.45  		val xs = map (fn n => if n < strict_args then "x"^(str n) else "x"^(str n)^"()") rightargs
   52.46 @@ -374,7 +374,7 @@
   52.47  		"structure "^name^" = struct",
   52.48  		"",
   52.49  		"datatype Term = Const of int | App of Term * Term | Abs of (Term -> Term)",
   52.50 -		"         "^(concat (map (fn c => " | C"^(str c)^(mk_constr_type_args (the (arity_of c)))) constants)),
   52.51 +		"         "^(implode (map (fn c => " | C"^(str c)^(mk_constr_type_args (the (arity_of c)))) constants)),
   52.52  		""]
   52.53  	fun make_constr c argprefix = "(C"^(str c)^" "^(string_of_tuple (map (fn i => argprefix^(str i)) (section (the (arity_of c)))))^")"
   52.54  	fun make_term_eq c = "  | term_eq "^(make_constr c "a")^" "^(make_constr c "b")^" = "^
   52.55 @@ -385,7 +385,7 @@
   52.56  				      val eqs = map (fn i => "term_eq a"^(str i)^" b"^(str i)) (section n)
   52.57  				      val (eq, eqs) = (List.hd eqs, map (fn s => " andalso "^s) (List.tl eqs))
   52.58  				  in
   52.59 -				      eq^(concat eqs)
   52.60 +				      eq^(implode eqs)
   52.61  				  end)
   52.62  	val _ = writelist [
   52.63  		"fun term_eq (Const c1) (Const c2) = (c1 = c2)",
   52.64 @@ -421,7 +421,7 @@
   52.65  							(gnum, r::l)::rs
   52.66  						    else
   52.67  							let
   52.68 -							    val args = concat (map (fn i => " a"^(str i)) (section (the (arity_of c))))
   52.69 +							    val args = implode (map (fn i => " a"^(str i)) (section (the (arity_of c))))
   52.70  							    fun gnumc g = if g > 0 then "c"^(str c)^"_"^(str g)^args else "c"^(str c)^args
   52.71  							    val s = gnumc (gnum) ^ " = " ^ gnumc (gnum') 
   52.72  							in
   52.73 @@ -444,7 +444,7 @@
   52.74  		val leftargs = 
   52.75  		    case args of
   52.76  			[] => ""
   52.77 -		      | (x::xs) => "("^x^(concat (map (fn s => ", "^s) xs))^")"
   52.78 +		      | (x::xs) => "("^x^(implode (map (fn s => ", "^s) xs))^")"
   52.79  		val args = map (indexed "convert a") (section (the (arity_of c)))
   52.80  		val right = fold (fn x => fn s => "AM_SML.App ("^s^", "^x^")") args ("AM_SML.Const "^(str c))
   52.81  	    in
    53.1 --- a/src/ZF/Tools/datatype_package.ML	Thu Oct 15 23:10:35 2009 +0200
    53.2 +++ b/src/ZF/Tools/datatype_package.ML	Thu Oct 15 23:28:10 2009 +0200
    53.3 @@ -146,13 +146,13 @@
    53.4    val (_, case_lists) = List.foldr add_case_list (1,[]) con_ty_lists;
    53.5  
    53.6    (*extract the types of all the variables*)
    53.7 -  val case_typ = List.concat (map (map (#2 o #1)) con_ty_lists) ---> @{typ "i => i"};
    53.8 +  val case_typ = maps (map (#2 o #1)) con_ty_lists ---> @{typ "i => i"};
    53.9  
   53.10    val case_base_name = big_rec_base_name ^ "_case";
   53.11    val case_name = full_name case_base_name;
   53.12  
   53.13    (*The list of all the function variables*)
   53.14 -  val case_args = List.concat (map (map #1) case_lists);
   53.15 +  val case_args = maps (map #1) case_lists;
   53.16  
   53.17    val case_const = Const (case_name, case_typ);
   53.18    val case_tm = list_comb (case_const, case_args);
   53.19 @@ -218,19 +218,18 @@
   53.20    val (_, recursor_lists) = List.foldr add_case_list (1,[]) rec_ty_lists;
   53.21  
   53.22    (*extract the types of all the variables*)
   53.23 -  val recursor_typ = List.concat (map (map (#2 o #1)) rec_ty_lists) ---> @{typ "i => i"};
   53.24 +  val recursor_typ = maps (map (#2 o #1)) rec_ty_lists ---> @{typ "i => i"};
   53.25  
   53.26    val recursor_base_name = big_rec_base_name ^ "_rec";
   53.27    val recursor_name = full_name recursor_base_name;
   53.28  
   53.29    (*The list of all the function variables*)
   53.30 -  val recursor_args = List.concat (map (map #1) recursor_lists);
   53.31 +  val recursor_args = maps (map #1) recursor_lists;
   53.32  
   53.33    val recursor_tm =
   53.34      list_comb (Const (recursor_name, recursor_typ), recursor_args);
   53.35  
   53.36 -  val recursor_cases = map call_recursor
   53.37 -                         (List.concat case_lists ~~ List.concat recursor_lists)
   53.38 +  val recursor_cases = map call_recursor (flat case_lists ~~ flat recursor_lists);
   53.39  
   53.40    val recursor_def =
   53.41        PrimitiveDefs.mk_defpair
   53.42 @@ -252,16 +251,15 @@
   53.43    val (con_defs, thy0) = thy_path
   53.44               |> Sign.add_consts_i
   53.45                   (map (fn (c, T, mx) => (Binding.name c, T, mx))
   53.46 -                  ((case_base_name, case_typ, NoSyn) :: map #1 (List.concat con_ty_lists)))
   53.47 +                  ((case_base_name, case_typ, NoSyn) :: map #1 (flat con_ty_lists)))
   53.48               |> PureThy.add_defs false
   53.49                   (map (Thm.no_attributes o apfst Binding.name)
   53.50                    (case_def ::
   53.51 -                   List.concat (ListPair.map mk_con_defs
   53.52 -                         (1 upto npart, con_ty_lists))))
   53.53 +                   flat (ListPair.map mk_con_defs (1 upto npart, con_ty_lists))))
   53.54               ||> add_recursor
   53.55               ||> Sign.parent_path
   53.56  
   53.57 -  val intr_names = map (Binding.name o #2) (List.concat con_ty_lists);
   53.58 +  val intr_names = map (Binding.name o #2) (flat con_ty_lists);
   53.59    val (thy1, ind_result) =
   53.60      thy0 |> Ind_Package.add_inductive_i
   53.61        false (rec_tms, dom_sum) (map Thm.no_attributes (intr_names ~~ intr_tms))
   53.62 @@ -296,9 +294,7 @@
   53.63  
   53.64    val free_iffs = map standard (con_defs RL [@{thm def_swap_iff}]);
   53.65  
   53.66 -  val case_eqns =
   53.67 -      map prove_case_eqn
   53.68 -         (List.concat con_ty_lists ~~ case_args ~~ tl con_defs);
   53.69 +  val case_eqns = map prove_case_eqn (flat con_ty_lists ~~ case_args ~~ tl con_defs);
   53.70  
   53.71    (*** Prove the recursor theorems ***)
   53.72  
   53.73 @@ -336,7 +332,7 @@
   53.74                 simp_tac (rank_ss addsimps case_eqns) 1,
   53.75                 IF_UNSOLVED (simp_tac (rank_ss addsimps tl con_defs) 1)]);
   53.76        in
   53.77 -         map prove_recursor_eqn (List.concat con_ty_lists ~~ recursor_cases)
   53.78 +         map prove_recursor_eqn (flat con_ty_lists ~~ recursor_cases)
   53.79        end
   53.80  
   53.81    val constructors =
    54.1 --- a/src/ZF/Tools/induct_tacs.ML	Thu Oct 15 23:10:35 2009 +0200
    54.2 +++ b/src/ZF/Tools/induct_tacs.ML	Thu Oct 15 23:28:10 2009 +0200
    54.3 @@ -74,7 +74,7 @@
    54.4    let fun mk_pair (Const(@{const_name mem},_) $ Free (v,_) $ A) =
    54.5               (v, #1 (dest_Const (head_of A)))
    54.6          | mk_pair _ = raise Match
    54.7 -      val pairs = List.mapPartial (try (mk_pair o FOLogic.dest_Trueprop))
    54.8 +      val pairs = map_filter (try (mk_pair o FOLogic.dest_Trueprop))
    54.9            (#2 (OldGoals.strip_context Bi))
   54.10    in case AList.lookup (op =) pairs var of
   54.11         NONE => raise Find_tname ("Cannot determine datatype of " ^ quote var)
    55.1 --- a/src/ZF/ind_syntax.ML	Thu Oct 15 23:10:35 2009 +0200
    55.2 +++ b/src/ZF/ind_syntax.ML	Thu Oct 15 23:28:10 2009 +0200
    55.3 @@ -89,7 +89,7 @@
    55.4  	               $ rec_tm))
    55.5    in  map mk_intr constructs  end;
    55.6  
    55.7 -fun mk_all_intr_tms sg arg = List.concat (ListPair.map (mk_intr_tms sg) arg);
    55.8 +fun mk_all_intr_tms sg arg = flat (ListPair.map (mk_intr_tms sg) arg);
    55.9  
   55.10  fun mk_Un (t1, t2) = @{const Un} $ t1 $ t2;
   55.11  
    56.1 --- a/src/ZF/simpdata.ML	Thu Oct 15 23:10:35 2009 +0200
    56.2 +++ b/src/ZF/simpdata.ML	Thu Oct 15 23:28:10 2009 +0200
    56.3 @@ -16,9 +16,8 @@
    56.4            case head_of t of
    56.5                Const(a,_) =>
    56.6                  (case AList.lookup (op =) pairs a of
    56.7 -                     SOME rls => List.concat (map (atomize (conn_pairs, mem_pairs))
    56.8 -                                       ([th] RL rls))
    56.9 -                   | NONE     => [th])
   56.10 +                     SOME rls => maps (atomize (conn_pairs, mem_pairs)) ([th] RL rls)
   56.11 +                   | NONE => [th])
   56.12              | _ => [th]
   56.13    in case concl_of th of
   56.14           Const("Trueprop",_) $ P =>