1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Thu Jul 29 18:45:41 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Thu Jul 29 19:03:46 2010 +0200
     1.3 @@ -34,7 +34,10 @@
     1.4    let val n = length name_thms_pairs in
     1.5      string_of_int n ^ " theorem" ^ plural_s n ^
     1.6      (if n > 0 then
     1.7 -       ": " ^ space_implode " " (sort_distinct string_ord name_thms_pairs)
     1.8 +       ": " ^ space_implode " "
     1.9 +                  (name_thms_pairs
    1.10 +                   |> map (perhaps (try (unprefix chained_prefix)))
    1.11 +                   |> sort_distinct string_ord)
    1.12       else
    1.13         "")
    1.14    end
    1.15 @@ -65,7 +68,8 @@
    1.16  
    1.17  (* minimalization of thms *)
    1.18  
    1.19 -fun filter_used_facts used = filter (member (op =) used o fst)
    1.20 +fun filter_used_facts used =
    1.21 +  filter (member (op =) used o perhaps (try (unprefix chained_prefix)) o fst)
    1.22  
    1.23  fun sublinear_minimize _ [] p = p
    1.24    | sublinear_minimize test (x :: xs) (seen, result) =