# HG changeset patch
# User blanchet
# Date 1280423026 -7200
# Node ID ff1d4078fe9ab410b5d0c01a73f8612771184767
# Parent  81a003f7de0dfde4e981086989be774fc1069a1c
deal with chained facts more gracefully

diff -r 81a003f7de0d -r ff1d4078fe9a src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Thu Jul 29 18:45:41 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Thu Jul 29 19:03:46 2010 +0200
@@ -34,7 +34,10 @@
   let val n = length name_thms_pairs in
     string_of_int n ^ " theorem" ^ plural_s n ^
     (if n > 0 then
-       ": " ^ space_implode " " (sort_distinct string_ord name_thms_pairs)
+       ": " ^ space_implode " "
+                  (name_thms_pairs
+                   |> map (perhaps (try (unprefix chained_prefix)))
+                   |> sort_distinct string_ord)
      else
        "")
   end
@@ -65,7 +68,8 @@
 
 (* minimalization of thms *)
 
-fun filter_used_facts used = filter (member (op =) used o fst)
+fun filter_used_facts used =
+  filter (member (op =) used o perhaps (try (unprefix chained_prefix)) o fst)
 
 fun sublinear_minimize _ [] p = p
   | sublinear_minimize test (x :: xs) (seen, result) =