changeset 60754 | 02924903a6fd |
parent 59530 | 2a20354c0877 |
child 61144 | 5e94dfead1c2 |
--- a/src/Provers/Arith/cancel_numeral_factor.ML Sat Jul 18 20:53:05 2015 +0200 +++ b/src/Provers/Arith/cancel_numeral_factor.ML Sat Jul 18 20:54:56 2015 +0200 @@ -72,7 +72,7 @@ in Option.map (export o Data.simplify_meta_eq ctxt) (Data.prove_conv - [Data.trans_tac ctxt reshape, rtac Data.cancel 1, + [Data.trans_tac ctxt reshape, resolve_tac ctxt [Data.cancel] 1, Data.numeral_simp_tac ctxt] ctxt prems (t', rhs)) end (* FIXME avoid handling of generic exceptions *)