src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
changeset 36393 be73a2b2443b
parent 36382 b90fc0d75bca
child 36402 1b20805974c7
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Sun Apr 25 10:22:31 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Sun Apr 25 11:38:46 2010 +0200
     1.3 @@ -92,13 +92,14 @@
     1.4    in
     1.5      (* try prove first to check result and get used theorems *)
     1.6      (case test_thms_fun NONE name_thms_pairs of
     1.7 -      result as {outcome = NONE, internal_thm_names, filtered_clauses, ...} =>
     1.8 +      result as {outcome = NONE, pool, internal_thm_names, filtered_clauses,
     1.9 +                 ...} =>
    1.10          let
    1.11            val used = internal_thm_names |> Vector.foldr (op ::) []
    1.12                                          |> sort_distinct string_ord
    1.13            val to_use =
    1.14              if length used < length name_thms_pairs then
    1.15 -              filter (fn (name1, _) => List.exists (curry (op =) name1) used)
    1.16 +              filter (fn (name1, _) => exists (curry (op =) name1) used)
    1.17                       name_thms_pairs
    1.18              else name_thms_pairs
    1.19            val (min_thms, {proof, internal_thm_names, ...}) =
    1.20 @@ -109,7 +110,7 @@
    1.21              ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ ".")
    1.22          in
    1.23            (SOME min_thms,
    1.24 -           proof_text isar_proof debug modulus sorts ctxt
    1.25 +           proof_text isar_proof pool debug modulus sorts ctxt
    1.26                        (K "", proof, internal_thm_names, goal, i) |> fst)
    1.27          end
    1.28      | {outcome = SOME TimedOut, ...} =>