# HG changeset patch
# User blanchet
# Date 1284648882 -7200
# Node ID a52a4e4399c19b1e30630ee1325923e5f36a32f9
# Parent  bb4fb9ffe2d173d90507123a3bda09870accf992
got caught once again by SML's pattern maching (ctor vs. var)

diff -r bb4fb9ffe2d1 -r a52a4e4399c1 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Sep 16 16:24:23 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Sep 16 16:54:42 2010 +0200
@@ -20,6 +20,7 @@
 structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE =
 struct
 
+open ATP_Proof
 open Sledgehammer_Util
 open Sledgehammer_Filter
 open Sledgehammer_Translate
@@ -28,9 +29,9 @@
 
 (* wrapper for calling external prover *)
 
-fun string_for_failure ATP_Proof.Unprovable = "Unprovable."
-  | string_for_failure ATP_Proof.TimedOut = "Timed out."
-  | string_for_failure ATP_Proof.Interrupted = "Interrupted."
+fun string_for_failure Unprovable = "Unprovable."
+  | string_for_failure TimedOut = "Timed out."
+  | string_for_failure Interrupted = "Interrupted."
   | string_for_failure _ = "Unknown error."
 
 fun n_theorems names =