diff -r e01e2328d0f0 -r 4f7975c74cdf src/HOL/Integ/IntDef.ML
--- a/src/HOL/Integ/IntDef.ML	Mon Jan 11 12:52:53 1999 +0100
+++ b/src/HOL/Integ/IntDef.ML	Mon Jan 11 16:50:49 1999 +0100
@@ -149,7 +149,6 @@
 
 Goalw [neg_def, int_def] "~ neg(int n)";
 by (Simp_tac 1);
-by Safe_tac;
 qed "not_neg_nat";
 
 Goalw [neg_def, int_def] "neg(- (int (Suc n)))";