# HG changeset patch # User nipkow # Date 1252655582 -7200 # Node ID c4a12569de89668e126c7a082453dc26a951a3d7 # Parent fdbfa0e35e786df6d3565d568af3b5fa5bcf895b# Parent b7a7b535d60735362795805f3ce9a9d0c776b5c1 merged diff -r fdbfa0e35e78 -r c4a12569de89 src/HOL/Mirabelle/Tools/mirabelle_metis.ML --- 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