diff -r 3e32fa0e779a -r 9769afcc1c4e arith.ML
--- a/arith.ML	Tue Jan 04 18:33:20 1994 +0100
+++ b/arith.ML	Wed Jan 05 19:37:07 1994 +0100
@@ -32,9 +32,9 @@
 
 (*** Simplification over add, mult, diff ***)
 
-val arith_simps = [add_0, add_Suc,
-		  mult_0, mult_Suc,
-		  diff_0, diff_0_eq_0, diff_Suc_Suc];
+val arith_simps =
+ [pred_0, pred_Suc, add_0, add_Suc, mult_0, mult_Suc,
+  diff_0, diff_0_eq_0, diff_Suc_Suc];
 
 val arith_ss = nat_ss addsimps arith_simps;
 
@@ -201,7 +201,7 @@
 
 goal Arith.thy "P(k) --> (!n. P(Suc(n))--> P(n)) --> P(k-i)";
 by (res_inst_tac [("m","k"),("n","i")] diff_induct 1);
-by (ALLGOALS (strip_tac THEN' simp_tac arith_ss THEN' fast_tac HOL_cs));
+by (ALLGOALS (strip_tac THEN' simp_tac arith_ss THEN' TRY o fast_tac HOL_cs));
 val zero_induct_lemma = result();
 
 val prems = goal Arith.thy "[| P(k);  !!n. P(Suc(n)) ==> P(n) |] ==> P(0)";