src/ZF/arith_data.ML

--- a/src/ZF/arith_data.ML	Tue Feb 10 14:29:36 2015 +0100
+++ b/src/ZF/arith_data.ML	Tue Feb 10 14:48:26 2015 +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 (resolve_tac [th RS th2]);
+  | gen_trans_tac th2 (SOME th) = ALLGOALS (resolve0_tac [th RS th2]);
 
 (*Use <-> or = depending on the type of t*)
 fun mk_eq_iff(t,u) =