diff -r c2cd79a6645f -r 678999604ee9 src/HOL/Auth/OtwayRees_AN.ML
--- a/src/HOL/Auth/OtwayRees_AN.ML	Tue Sep 22 17:08:30 1998 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.ML	Wed Sep 23 10:03:32 1998 +0200
@@ -230,7 +230,7 @@
 by (ALLGOALS
     (asm_simp_tac (simpset() addcongs [conj_cong, if_weak_cong] 
                              addsimps [analz_insert_eq, analz_insert_freshK]
-                             addsimps (pushes@split_ifs))));
+                                      @ pushes @ split_ifs)));
 (*Oops*)
 by (blast_tac (claset() addSDs [unique_session_keys]) 4);
 (*OR4*)