diff -r 01c4d14b2a61 -r 6628adcae4a7 src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML	Thu Aug 26 09:23:21 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML	Thu Aug 26 10:42:06 2010 +0200
@@ -7,11 +7,12 @@
 
 signature SLEDGEHAMMER_FACT_MINIMIZE =
 sig
+  type locality = Sledgehammer_Fact_Filter.locality
   type params = Sledgehammer.params
 
   val minimize_theorems :
-    params -> int -> int -> Proof.state -> ((string * bool) * thm list) list
-    -> ((string * bool) * thm list) list option * string
+    params -> int -> int -> Proof.state -> ((string * locality) * thm list) list
+    -> ((string * locality) * thm list) list option * string
   val run_minimize : params -> int -> Facts.ref list -> Proof.state -> unit
 end;
 
@@ -120,7 +121,7 @@
          val n = length min_thms
          val _ = priority (cat_lines
            ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^
-            (case length (filter (snd o fst) min_thms) of
+            (case length (filter (curry (op =) Chained o snd o fst) min_thms) of
                0 => ""
              | n => " (including " ^ Int.toString n ^ " chained)") ^ ".")
        in
@@ -149,7 +150,7 @@
     val reserved = reserved_isar_keyword_table ()
     val chained_ths = #facts (Proof.goal state)
     val axioms =
-      maps (map (fn (name, (_, th)) => (name (), [th]))
+      maps (map (apsnd single)
             o name_thm_pairs_from_ref ctxt reserved chained_ths) refs
   in
     case subgoal_count state of