src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
changeset 36402 1b20805974c7
parent 36393 be73a2b2443b
child 36481 af99c98121d6
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Mon Apr 26 21:18:20 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Mon Apr 26 21:20:43 2010 +0200
     1.3 @@ -68,7 +68,7 @@
     1.4  (* minimalization of thms *)
     1.5  
     1.6  fun minimize_theorems (params as {debug, atps, minimize_timeout, isar_proof,
     1.7 -                                  modulus, sorts, ...})
     1.8 +                                  shrink_factor, sorts, ...})
     1.9                        i state name_thms_pairs =
    1.10    let
    1.11      val thy = Proof.theory_of state
    1.12 @@ -92,8 +92,8 @@
    1.13    in
    1.14      (* try prove first to check result and get used theorems *)
    1.15      (case test_thms_fun NONE name_thms_pairs of
    1.16 -      result as {outcome = NONE, pool, internal_thm_names, filtered_clauses,
    1.17 -                 ...} =>
    1.18 +      result as {outcome = NONE, pool, internal_thm_names, conjecture_shape,
    1.19 +                 filtered_clauses, ...} =>
    1.20          let
    1.21            val used = internal_thm_names |> Vector.foldr (op ::) []
    1.22                                          |> sort_distinct string_ord
    1.23 @@ -110,7 +110,9 @@
    1.24              ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ ".")
    1.25          in
    1.26            (SOME min_thms,
    1.27 -           proof_text isar_proof pool debug modulus sorts ctxt
    1.28 +           proof_text isar_proof
    1.29 +                      (pool, debug, shrink_factor, sorts, ctxt,
    1.30 +                       conjecture_shape)
    1.31                        (K "", proof, internal_thm_names, goal, i) |> fst)
    1.32          end
    1.33      | {outcome = SOME TimedOut, ...} =>