| changeset 32469 | 1ad7d4fc0954 |
| parent 32385 | 594890623c46 |
| child 32472 | 7b92a8b8daaf |
--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_arith.ML Mon Aug 31 19:28:37 2009 +0200 +++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_arith.ML Tue Sep 01 14:09:59 2009 +0200 @@ -5,8 +5,8 @@ structure Mirabelle_Arith : MIRABELLE_ACTION = struct -fun arith_action {pre=st, ...} = - if Mirabelle.can_apply Arith_Data.arith_tac st +fun arith_action timeout {pre=st, ...} = + if Mirabelle.can_apply timeout Arith_Data.arith_tac st then SOME "succeeded" else NONE