src/FOL/ex/nat.ML

--- a/src/FOL/ex/nat.ML	Fri Nov 19 11:34:31 1993 +0100
+++ b/src/FOL/ex/nat.ML	Fri Nov 19 11:35:59 1993 +0100
@@ -43,7 +43,7 @@
 by (resolve_tac [rec_Suc] 1);
 val add_Suc = result();
 
-val add_ss = FOL_ss  addsimps  [add_0, add_Suc];
+val add_ss = FOL_ss addsimps [add_0, add_Suc];
 
 goal Nat.thy "(k+m)+n = k+(m+n)";
 by (res_inst_tac [("n","k")] induct 1);