--- a/src/HOL/Arith.ML Mon Sep 29 11:36:44 1997 +0200
+++ b/src/HOL/Arith.ML Mon Sep 29 11:37:02 1997 +0200
@@ -403,7 +403,7 @@
Addsimps [diff_add_inverse2];
goal Arith.thy "!!i j k::nat. i<=j ==> (j-i=k) = (j=k+i)";
-by (Step_tac 1);
+by Safe_tac;
by (ALLGOALS Asm_simp_tac);
qed "le_imp_diff_is_add";
@@ -546,7 +546,7 @@
goal Arith.thy "!!k. 0<k ==> (m*k = n*k) = (m=n)";
by (cut_facts_tac [less_linear] 1);
-by (Step_tac 1);
+by Safe_tac;
by (assume_tac 2);
by (ALLGOALS (dtac mult_less_mono1 THEN' assume_tac));
by (ALLGOALS Asm_full_simp_tac);