--- a/src/Pure/pure_thy.ML Thu Apr 27 12:11:56 2006 +0200
+++ b/src/Pure/pure_thy.ML Thu Apr 27 15:06:35 2006 +0200
@@ -219,7 +219,7 @@
error ("Bad subscript " ^ string_of_int i ^ " for " ^
quote name ^ " (length " ^ string_of_int n ^ ")")
else List.nth (thms, i - 1);
- in map select (List.concat (map (interval n) is)) end;
+ in map select (maps (interval n) is) end;
(* selections *)
@@ -263,7 +263,7 @@
|> the_thms name |> select_thm thmref |> map (Thm.transfer theory)
end;
-fun get_thmss thy thmrefs = List.concat (map (get_thms thy) thmrefs);
+fun get_thmss thy thmrefs = maps (get_thms thy) thmrefs;
fun get_thm thy thmref = single_thm (name_of_thmref thmref) (get_thms thy thmref);
fun thm name = get_thm (the_context ()) (Name name);
@@ -279,14 +279,13 @@
fun thms_containing theory spec =
(theory :: Theory.ancestors_of theory)
- |> map (fn thy =>
+ |> maps (fn thy =>
FactIndex.find (fact_index_of thy) spec
|> List.filter (fn (name, ths) => valid_thms theory (Name name, ths))
- |> distinct (eq_fst (op =)))
- |> List.concat;
+ |> distinct (eq_fst (op =)));
fun thms_containing_consts thy consts =
- thms_containing thy (consts, []) |> map #2 |> List.concat
+ thms_containing thy (consts, []) |> maps #2
|> map (fn th => (Thm.name_of_thm th, th));
@@ -294,9 +293,9 @@
fun thms_of thy =
let val thms = #2 (theorems_of thy)
- in map (fn th => (Thm.name_of_thm th, th)) (List.concat (map snd (Symtab.dest thms))) end;
+ in map (fn th => (Thm.name_of_thm th, th)) (maps snd (Symtab.dest thms)) end;
-fun all_thms_of thy = List.concat (map thms_of (thy :: Theory.ancestors_of thy));
+fun all_thms_of thy = maps thms_of (thy :: Theory.ancestors_of thy);
@@ -379,7 +378,7 @@
let
fun app (x, (ths, atts)) = foldl_map (Thm.theory_attributes atts) (x, ths);
val (thms, thy') = thy |> enter_thms
- name_thmss (name_thms false) (apsnd List.concat o foldl_map app)
+ name_thmss (name_thms false) (apsnd flat o foldl_map app)
(bname, map (fn (ths, atts) => (get thy ths, atts @ more_atts @ [kind k])) ths_atts);
in ((bname, thms), thy') end);