author | nipkow |
Fri, 11 Sep 2009 09:53:02 +0200 | |
changeset 32563 | c4a12569de89 |
parent 32561 | fdbfa0e35e78 (current diff) |
parent 32562 | b7a7b535d607 (diff) |
child 32564 | 378528d2f7eb |
--- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Fri Sep 11 09:05:26 2009 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Fri Sep 11 09:53:02 2009 +0200 @@ -10,7 +10,7 @@ fun init _ = I fun done _ _ = () -fun run id {pre, post, timeout, log} = +fun run id {pre, post, timeout, log, ...} = let val thms = Mirabelle.theorems_of_sucessful_proof post val names = map Thm.get_name thms