src/HOL/Auth/OtwayRees_Bad.ML
changeset 5535 678999604ee9
parent 5492 d9fc3457554e
child 6308 76f3865a2b1d
--- a/src/HOL/Auth/OtwayRees_Bad.ML	Tue Sep 22 17:08:30 1998 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.ML	Wed Sep 23 10:03:32 1998 +0200
@@ -199,7 +199,7 @@
 by (ALLGOALS
     (asm_simp_tac (simpset() addcongs [conj_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*)