# HG changeset patch # User nipkow # Date 1252655560 -7200 # Node ID b7a7b535d60735362795805f3ce9a9d0c776b5c1 # Parent 4d4ee06e9420713aa84a7e5c9d5c2f5255c480af Made record parameter flexible to allow for extensions diff -r 4d4ee06e9420 -r b7a7b535d607 src/HOL/Mirabelle/Tools/mirabelle_metis.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Thu Sep 10 16:16:18 2009 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Fri Sep 11 09:52:40 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