| 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 ()