# HG changeset patch
# User wenzelm
# Date 1294438024 -3600
# Node ID d3be2a414d15718f0d15c69053f8bf696fddfe71
# Parent  1db1b47cec3d01fbfb9bcbb5c5b27dab0642a514
tuned;

diff -r 1db1b47cec3d -r d3be2a414d15 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
--- 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
diff -r 1db1b47cec3d -r d3be2a414d15 src/Tools/WWW_Find/xhtml.ML
--- 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)