--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Fri Jan 07 23:02:12 2011 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Fri Jan 07 23:07:04 2011 +0100
@@ -130,7 +130,7 @@
relevance_fudge relevance_override facts hyp_ts concl_t
|> map (fst o fst)
val (found_facts, lost_facts) =
- List.concat proofs |> sort_distinct string_ord
+ flat proofs |> sort_distinct string_ord
|> map (fn fact => (find_index (curry (op =) fact) facts, fact))
|> List.partition (curry (op <=) 0 o fst)
|>> sort (prod_ord int_ord string_ord) ||> map snd
--- a/src/Tools/WWW_Find/xhtml.ML Fri Jan 07 23:02:12 2011 +0100
+++ b/src/Tools/WWW_Find/xhtml.ML Fri Jan 07 23:07:04 2011 +0100
@@ -183,7 +183,7 @@
@
(if length inner = 0
then ["/>"]
- else List.concat (
+ else flat (
[[">"]]
@
map show inner
@@ -304,7 +304,7 @@
fun to_dtdd (nm, tag) = [Tag ("dt", [], [Text nm]),
Tag ("dd", [], [tag])];
fun dl (common_atts, dtdds) =
- Tag ("dl", from_common common_atts, (List.concat o map to_dtdd) dtdds);
+ Tag ("dl", from_common common_atts, maps to_dtdd dtdds);
fun alternate_class { class0, class1 } rows = let
fun f ((true, xs), x) = (false, add_attributes [("class", class0)] x :: xs)