changeset 43212 | 050a03afe024 |
parent 43205 | 23b81469499f |
child 44651 | 5d6a11e166cf |
--- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Mon Jun 06 20:36:36 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Mon Jun 06 20:56:06 2011 +0200 @@ -18,7 +18,7 @@ val facts = Facts.props (Proof_Context.facts_of (Proof.context_of pre)) - fun metis ctxt = Metis_Tactics.new_metis_tac [] ctxt (thms @ facts) + fun metis ctxt = Metis_Tactics.metis_tac [] ctxt (thms @ facts) in (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed") |> prefix (metis_tag id)