1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML	Thu Aug 26 09:23:21 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML	Thu Aug 26 10:42:06 2010 +0200
     1.3 @@ -7,11 +7,12 @@
     1.4  
     1.5  signature SLEDGEHAMMER_FACT_MINIMIZE =
     1.6  sig
     1.7 +  type locality = Sledgehammer_Fact_Filter.locality
     1.8    type params = Sledgehammer.params
     1.9  
    1.10    val minimize_theorems :
    1.11 -    params -> int -> int -> Proof.state -> ((string * bool) * thm list) list
    1.12 -    -> ((string * bool) * thm list) list option * string
    1.13 +    params -> int -> int -> Proof.state -> ((string * locality) * thm list) list
    1.14 +    -> ((string * locality) * thm list) list option * string
    1.15    val run_minimize : params -> int -> Facts.ref list -> Proof.state -> unit
    1.16  end;
    1.17  
    1.18 @@ -120,7 +121,7 @@
    1.19           val n = length min_thms
    1.20           val _ = priority (cat_lines
    1.21             ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^
    1.22 -            (case length (filter (snd o fst) min_thms) of
    1.23 +            (case length (filter (curry (op =) Chained o snd o fst) min_thms) of
    1.24                 0 => ""
    1.25               | n => " (including " ^ Int.toString n ^ " chained)") ^ ".")
    1.26         in
    1.27 @@ -149,7 +150,7 @@
    1.28      val reserved = reserved_isar_keyword_table ()
    1.29      val chained_ths = #facts (Proof.goal state)
    1.30      val axioms =
    1.31 -      maps (map (fn (name, (_, th)) => (name (), [th]))
    1.32 +      maps (map (apsnd single)
    1.33              o name_thm_pairs_from_ref ctxt reserved chained_ths) refs
    1.34    in
    1.35      case subgoal_count state of