# 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