diff -r e84d900cd287 -r 59203adfc33f src/ZF/arith_data.ML
--- a/src/ZF/arith_data.ML	Thu Oct 30 16:20:46 2014 +0100
+++ b/src/ZF/arith_data.ML	Thu Oct 30 16:55:29 2014 +0100
@@ -51,7 +51,7 @@
 
 (*Apply the given rewrite (if present) just once*)
 fun gen_trans_tac th2 NONE      = all_tac
-  | gen_trans_tac th2 (SOME th) = ALLGOALS (rtac (th RS th2));
+  | gen_trans_tac th2 (SOME th) = ALLGOALS (resolve_tac [th RS th2]);
 
 (*Use <-> or = depending on the type of t*)
 fun mk_eq_iff(t,u) =