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_atp.ML
changeset 55307 59ab33f9d4de
parent 55297 1dfcd49f5dcb
child 55308 dc68f6fb88d2 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Feb 03 19:50:38 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Feb 03 23:20:12 2014 +0100
@@ -372,7 +372,7 @@
                       |> factify_atp_proof fact_names hyp_ts concl_t
                   in
                     (verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress_isar,
-                     try0_isar, minimize |> the_default true, atp_proof, goal)
+                     try0_isar, minimize <> SOME false, atp_proof, goal)
                   end
                 val one_line_params =
                   (preplay, proof_banner mode name, used_facts,
isabelle