1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Wed Jul 28 19:23:56 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Wed Jul 28 19:42:11 2010 +0200
     1.3 @@ -9,6 +9,9 @@
     1.4  sig
     1.5    type params = Sledgehammer.params
     1.6  
     1.7 +  val minimize_theorems :
     1.8 +    params -> int -> int -> Proof.state -> (string * thm list) list
     1.9 +    -> (string * thm list) list option * string
    1.10    val run_minimizer : params -> int -> Facts.ref list -> Proof.state -> unit
    1.11  end;
    1.12