# HG changeset patch
# User blanchet
# Date 1284500316 -7200
# Node ID 9e544eb396dcc57f0ca771bd86ee2e813ae1c485
# Parent  ca81b7ae543c906622664bb4170e2127a085f784
tuning

diff -r ca81b7ae543c -r 9e544eb396dc src/HOL/Mirabelle/Tools/mirabelle.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Tue Sep 14 23:38:20 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Tue Sep 14 23:38:36 2010 +0200
@@ -160,7 +160,7 @@
     val full_tac = HEADGOAL (Method.insert_tac facts THEN' tac ctxt)
   in
     (case TimeLimit.timeLimit time (Seq.pull o full_tac) goal of
-      SOME (thm, _) => true
+      SOME _ => true
     | NONE => false)
   end
 
diff -r ca81b7ae543c -r 9e544eb396dc src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Sep 14 23:38:20 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Sep 14 23:38:36 2010 +0200
@@ -405,7 +405,7 @@
     case result of
       SH_OK (time_isa, time_atp, names) =>
         let
-          fun get_thms (name, Sledgehammer_Filter.Chained) = NONE
+          fun get_thms (_, Sledgehammer_Filter.Chained) = NONE
             | get_thms (name, loc) =
               SOME ((name, loc), thms_of_name (Proof.context_of st) name)
         in