1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Wed Apr 28 12:49:52 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Wed Apr 28 13:00:30 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 -                                  shrink_factor, sorts, ...})
     1.8 +                                  shrink_factor, ...})
     1.9                        i n state name_thms_pairs =
    1.10    let
    1.11      val thy = Proof.theory_of state
    1.12 @@ -109,8 +109,7 @@
    1.13          in
    1.14            (SOME min_thms,
    1.15             proof_text isar_proof
    1.16 -                      (pool, debug, shrink_factor, sorts, ctxt,
    1.17 -                       conjecture_shape)
    1.18 +                      (pool, debug, shrink_factor, ctxt, conjecture_shape)
    1.19                        (K "", proof, internal_thm_names, goal, i) |> fst)
    1.20          end
    1.21      | {outcome = SOME TimedOut, ...} =>