--- a/src/HOL/IOA/ABP/Action.ML	Wed Oct 04 13:11:57 1995 +0100
+++ b/src/HOL/IOA/ABP/Action.ML	Wed Oct 04 13:12:14 1995 +0100
@@ -8,6 +8,6 @@
 
 goal Action.thy "!!x. x = y ==> action_case a b c d e f g x =     \
 \                               action_case a b c d e f g y";
-by (asm_simp_tac HOL_ss 1);
+by (Asm_simp_tac 1);
 
-val action_ss = arith_ss addcongs [result()] addsimps Action.action.simps;
+Addcongs [result()];