Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuning
authorblanchet
Tue, 14 Sep 2010 23:38:36 +0200
changeset 39377 9e544eb396dc
parent 39376 ca81b7ae543c
child 39381 9717ea8d42b3
child 39384 76603e40bd4c
tuning
src/HOL/Mirabelle/Tools/mirabelle.ML file | annotate | diff | comparison | revisions
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML file | annotate | diff | comparison | revisions 
--- 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
 
--- 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
isabelle