tuned;
authorwenzelm
Fri Jan 07 23:07:04 2011 +0100 (2011-01-07)
changeset 41455d3be2a414d15
parent 41454 1db1b47cec3d
child 41456 006d85ad56d3
tuned;
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
src/Tools/WWW_Find/xhtml.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Fri Jan 07 23:02:12 2011 +0100
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Fri Jan 07 23:07:04 2011 +0100
     1.3 @@ -130,7 +130,7 @@
     1.4                 relevance_fudge relevance_override facts hyp_ts concl_t
     1.5             |> map (fst o fst)
     1.6           val (found_facts, lost_facts) =
     1.7 -           List.concat proofs |> sort_distinct string_ord
     1.8 +           flat proofs |> sort_distinct string_ord
     1.9             |> map (fn fact => (find_index (curry (op =) fact) facts, fact))
    1.10             |> List.partition (curry (op <=) 0 o fst)
    1.11             |>> sort (prod_ord int_ord string_ord) ||> map snd
     2.1 --- a/src/Tools/WWW_Find/xhtml.ML	Fri Jan 07 23:02:12 2011 +0100
     2.2 +++ b/src/Tools/WWW_Find/xhtml.ML	Fri Jan 07 23:07:04 2011 +0100
     2.3 @@ -183,7 +183,7 @@
     2.4     @
     2.5     (if length inner = 0
     2.6      then ["/>"]
     2.7 -    else List.concat (
     2.8 +    else flat (
     2.9        [[">"]]
    2.10        @
    2.11        map show inner
    2.12 @@ -304,7 +304,7 @@
    2.13  fun to_dtdd (nm, tag) = [Tag ("dt", [], [Text nm]),
    2.14                           Tag ("dd", [], [tag])];
    2.15  fun dl (common_atts, dtdds) =
    2.16 -  Tag ("dl", from_common common_atts, (List.concat o map to_dtdd) dtdds);
    2.17 +  Tag ("dl", from_common common_atts, maps to_dtdd dtdds);
    2.18              
    2.19  fun alternate_class { class0, class1 } rows = let
    2.20      fun f ((true, xs), x) = (false, add_attributes [("class", class0)] x :: xs)