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/Tools/Sledgehammer/sledgehammer_minimize.ML
changeset 40060 5ef6747aa619
parent 40059 6ad9081665db
child 40061 71cc5aac8b76 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Oct 21 14:55:09 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Oct 21 16:25:40 2010 +0200
@@ -96,7 +96,7 @@
                       i (_ : int) state axioms =
   let
     val thy = Proof.theory_of state
-    val atp = get_atp_fun thy prover
+    val atp = run_atp thy prover
     val msecs = Time.toMilliseconds timeout
     val _ = priority ("Sledgehammer minimize: prover " ^ quote prover ^ ".")
     val {context = ctxt, goal, ...} = Proof.goal state
isabelle