Made record parameter flexible to allow for extensions
authornipkow
Fri, 11 Sep 2009 09:52:40 +0200
changeset 32562 b7a7b535d607
parent 32552 4d4ee06e9420
child 32563 c4a12569de89
Made record parameter flexible to allow for extensions
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