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_prover_smt2.ML
changeset 57750 670cbec816b9
parent 57742 1977a884fef7
child 57776 1111a9a328fe 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -208,7 +208,7 @@
                  (verbose, (NONE, NONE), preplay_timeout, compress, try0, minimize, atp_proof (),
                   goal)
 
-               val one_line_params = (preplay, proof_banner mode name, subgoal, subgoal_count)
+               val one_line_params = (preplay (), proof_banner mode name, subgoal, subgoal_count)
                val num_chained = length (#facts (Proof.goal state))
              in
                proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained
isabelle