--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Wed Apr 28 12:49:52 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Wed Apr 28 13:00:30 2010 +0200
@@ -68,7 +68,7 @@
(* minimalization of thms *)
fun minimize_theorems (params as {debug, atps, minimize_timeout, isar_proof,
- shrink_factor, sorts, ...})
+ shrink_factor, ...})
i n state name_thms_pairs =
let
val thy = Proof.theory_of state
@@ -109,8 +109,7 @@
in
(SOME min_thms,
proof_text isar_proof
- (pool, debug, shrink_factor, sorts, ctxt,
- conjecture_shape)
+ (pool, debug, shrink_factor, ctxt, conjecture_shape)
(K "", proof, internal_thm_names, goal, i) |> fst)
end
| {outcome = SOME TimedOut, ...} =>