src/HOL/Auth/Recur.ML

--- a/src/HOL/Auth/Recur.ML	Tue Sep 22 17:08:30 1998 +0200
+++ b/src/HOL/Auth/Recur.ML	Wed Sep 23 10:03:32 1998 +0200
@@ -387,8 +387,7 @@
 by analz_spies_tac;
 by (ALLGOALS
     (asm_simp_tac
-     (simpset() addsimps (split_ifs @
-			 [analz_insert_eq, analz_insert_freshK]))));
+     (simpset() addsimps split_ifs @ [analz_insert_eq, analz_insert_freshK])));
 (*RA4*)
 by (spy_analz_tac 5);
 (*RA2*)