Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Mirabelle/Tools/mirabelle.ML
changeset 61841 4d3527b94f2a
parent 60361 88505460fde7
child 62505 9e2a65912111 
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Sun Dec 13 21:56:15 2015 +0100
@@ -154,7 +154,7 @@
 fun can_apply time tac st =
   let
     val {context = ctxt, facts, goal} = Proof.goal st
-    val full_tac = HEADGOAL (Method.insert_tac facts THEN' tac ctxt)
+    val full_tac = HEADGOAL (Method.insert_tac ctxt facts THEN' tac ctxt)
   in
     (case try (TimeLimit.timeLimit time (Seq.pull o full_tac)) goal of
       SOME (SOME _) => true
isabelle