# HG changeset patch
# User blanchet
# Date 1289220798 -3600
# Node ID 3d93bd33304dba83196d5e7674c5f446ea2c96d3
# Parent  b52912c228d47aea9299b3d0347f717919c5f717
compile -- 7550b2cba1cb broke the build

diff -r b52912c228d4 -r 3d93bd33304d src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Nov 08 13:25:00 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Nov 08 13:53:18 2010 +0100
@@ -434,16 +434,16 @@
       TimeLimit.timeLimit iter_timeout
           (SMT_Solver.smt_filter remote iter_timeout state facts) i
       handle TimeLimit.TimeOut =>
-             {outcome = SOME SMT_Solver.Time_Out, used_facts = [],
+             {outcome = SOME SMT_Failure.Time_Out, used_facts = [],
               run_time_in_msecs = NONE}
     val outcome0 = if is_none outcome0 then SOME outcome else outcome0
     val msecs_so_far = int_opt_add run_time_in_msecs msecs_so_far
     val too_many_facts_perhaps =
       case outcome of
         NONE => false
-      | SOME (SMT_Solver.Counterexample _) => false
-      | SOME SMT_Solver.Time_Out => iter_timeout <> timeout
-      | SOME SMT_Solver.Out_Of_Memory => true
+      | SOME (SMT_Failure.Counterexample _) => false
+      | SOME SMT_Failure.Time_Out => iter_timeout <> timeout
+      | SOME SMT_Failure.Out_Of_Memory => true
       | SOME _ => true
     val timeout = Time.- (timeout, Timer.checkRealTimer timer)
   in