src/HOL/Mirabelle/Tools/mirabelle_arith.ML
changeset 32567 de411627a985
parent 32564 378528d2f7eb
--- a/src/HOL/Mirabelle/Tools/mirabelle_arith.ML	Sun Sep 13 02:07:52 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_arith.ML	Sun Sep 13 02:10:41 2009 +0200
@@ -10,7 +10,7 @@
 fun init _ = I
 fun done _ _ = ()
 
-fun run id {pre, timeout, log, ...} =
+fun run id ({pre, timeout, log, ...}: Mirabelle.run_args) =
   if Mirabelle.can_apply timeout Arith_Data.arith_tac pre
   then log (arith_tag id ^ "succeeded")
   else ()