1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Sep 16 16:24:23 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Sep 16 16:54:42 2010 +0200
     1.3 @@ -20,6 +20,7 @@
     1.4  structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE =
     1.5  struct
     1.6  
     1.7 +open ATP_Proof
     1.8  open Sledgehammer_Util
     1.9  open Sledgehammer_Filter
    1.10  open Sledgehammer_Translate
    1.11 @@ -28,9 +29,9 @@
    1.12  
    1.13  (* wrapper for calling external prover *)
    1.14  
    1.15 -fun string_for_failure ATP_Proof.Unprovable = "Unprovable."
    1.16 -  | string_for_failure ATP_Proof.TimedOut = "Timed out."
    1.17 -  | string_for_failure ATP_Proof.Interrupted = "Interrupted."
    1.18 +fun string_for_failure Unprovable = "Unprovable."
    1.19 +  | string_for_failure TimedOut = "Timed out."
    1.20 +  | string_for_failure Interrupted = "Interrupted."
    1.21    | string_for_failure _ = "Unknown error."
    1.22  
    1.23  fun n_theorems names =