1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Thu Jul 29 12:07:09 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Thu Jul 29 14:39:43 2010 +0200
     1.3 @@ -18,7 +18,6 @@
     1.4  structure Sledgehammer_Fact_Minimizer : SLEDGEHAMMER_FACT_MINIMIZER =
     1.5  struct
     1.6  
     1.7 -open Metis_Clauses
     1.8  open Sledgehammer_Util
     1.9  open Sledgehammer_Fact_Filter
    1.10  open Sledgehammer_Proof_Reconstruct
    1.11 @@ -37,7 +36,7 @@
    1.12    | string_for_outcome (SOME failure) = string_for_failure failure
    1.13  
    1.14  fun sledgehammer_test_theorems (params : params) prover timeout subgoal state
    1.15 -                               filtered_clauses name_thms_pairs =
    1.16 +                               name_thms_pairs =
    1.17    let
    1.18      val num_theorems = length name_thms_pairs
    1.19      val _ =
    1.20 @@ -54,8 +53,7 @@
    1.21      val problem =
    1.22       {subgoal = subgoal, goal = (ctxt, (facts, goal)),
    1.23        relevance_override = {add = [], del = [], only = false},
    1.24 -      axiom_clauses = SOME name_thm_pairs,
    1.25 -      filtered_clauses = SOME (the_default name_thm_pairs filtered_clauses)}
    1.26 +      axiom_clauses = SOME name_thm_pairs}
    1.27    in
    1.28      prover params (K "") timeout problem
    1.29      |> tap (fn result : prover_result =>
    1.30 @@ -91,15 +89,14 @@
    1.31        sledgehammer_test_theorems params prover minimize_timeout i state
    1.32      val {context = ctxt, goal, ...} = Proof.goal state;
    1.33    in
    1.34 -    (* try prove first to check result and get used theorems *)
    1.35 -    (case test_facts NONE name_thms_pairs of
    1.36 -       result as {outcome = NONE, pool, proof, used_thm_names,
    1.37 -                  conjecture_shape, filtered_clauses, ...} =>
    1.38 +    (* FIXME: merge both "test_facts" calls *)
    1.39 +    (case test_facts name_thms_pairs of
    1.40 +       result as {outcome = NONE, pool, used_thm_names,
    1.41 +                  conjecture_shape, ...} =>
    1.42         let
    1.43           val (min_thms, {proof, internal_thm_names, ...}) =
    1.44 -           sublinear_minimize (test_facts (SOME filtered_clauses))
    1.45 -                              (filter_used_facts used_thm_names name_thms_pairs)
    1.46 -                              ([], result)
    1.47 +           sublinear_minimize test_facts
    1.48 +               (filter_used_facts used_thm_names name_thms_pairs) ([], result)
    1.49           val m = length min_thms
    1.50           val _ = priority (cat_lines
    1.51             ["Minimized: " ^ string_of_int m ^ " theorem" ^ plural_s m] ^ ".")