1.1 --- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_metis.ML	Wed Sep 02 16:02:37 2009 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,25 +0,0 @@
     1.4 -(* Title:  mirabelle_metis.ML
     1.5 -   Author: Jasmin Blanchette and Sascha Boehme
     1.6 -*)
     1.7 -
     1.8 -structure Mirabelle_Metis : MIRABELLE_ACTION =
     1.9 -struct
    1.10 -
    1.11 -fun metis_action {pre, post, timeout, log} =
    1.12 -  let
    1.13 -    val thms = Mirabelle.theorems_of_sucessful_proof post
    1.14 -    val names = map Thm.get_name thms
    1.15 -    val add_info = if null names then I else suffix (":\n" ^ commas names)
    1.16 -
    1.17 -    val facts = Facts.props (ProofContext.facts_of (Proof.context_of pre))
    1.18 -
    1.19 -    fun metis ctxt = MetisTools.metis_tac ctxt (thms @ facts)
    1.20 -  in
    1.21 -    (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed")
    1.22 -    |> add_info
    1.23 -    |> log
    1.24 -  end
    1.25 -
    1.26 -fun invoke _ = Mirabelle.register ("metis", metis_action)
    1.27 -
    1.28 -end