diff -r 130f3d891fb2 -r c2bd39a2c0ee src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Wed Sep 23 10:11:18 1998 +0200
+++ b/src/HOL/Arith.ML	Wed Sep 23 10:12:01 1998 +0200
@@ -202,8 +202,8 @@
 Goal "!!k:: nat. [| k<l;  m+l = k+n |] ==> m<n";
 by (auto_tac (claset(),
 	      simpset() delsimps [add_Suc_right]
-	                addsimps ([less_iff_Suc_add,
-				   add_Suc_right RS sym] @ add_ac)));
+	                addsimps [less_iff_Suc_add,
+				  add_Suc_right RS sym] @ add_ac));
 qed "less_add_eq_less";
 
 
@@ -378,7 +378,7 @@
 Goal "i<n ==> n - Suc i < n - i";
 by (exhaust_tac "n" 1);
 by (auto_tac (claset(),
-	      simpset() addsimps ([Suc_diff_le]@le_simps)));
+	      simpset() addsimps [Suc_diff_le]@le_simps));
 qed "diff_Suc_less_diff";
 
 Goal "m - n <= Suc m - n";
@@ -471,7 +471,7 @@
 
 Goal "(m+k) - (n+k) = m - (n::nat)";
 val add_commute_k = read_instantiate [("n","k")] add_commute;
-by (asm_simp_tac (simpset() addsimps ([add_commute_k])) 1);
+by (asm_simp_tac (simpset() addsimps [add_commute_k]) 1);
 qed "diff_cancel2";
 Addsimps [diff_cancel2];