src/ZF/Integ/Integ.ML

--- a/src/ZF/Integ/Integ.ML	Tue Sep 22 15:23:39 1998 +0200
+++ b/src/ZF/Integ/Integ.ML	Tue Sep 22 15:24:01 1998 +0200
@@ -144,8 +144,8 @@
 by Safe_tac;
 by (dres_inst_tac [("psi", "?lhs=?rhs")] asm_rl 1);
 by (dres_inst_tac [("psi", "?lhs<?rhs")] asm_rl 1);
-by (fast_tac (claset() addss
-              (simpset() addsimps [add_le_self2 RS le_imp_not_lt])) 1);
+by (force_tac (claset(),
+	       simpset() addsimps [add_le_self2 RS le_imp_not_lt]) 1);
 qed "not_znegative_znat";
 
 Addsimps [not_znegative_znat];