src/HOL/TLA/Memory/Memory.ML

--- a/src/HOL/TLA/Memory/Memory.ML	Thu Mar 12 13:15:36 1998 +0100
+++ b/src/HOL/TLA/Memory/Memory.ML	Thu Mar 12 13:17:13 1998 +0100
@@ -97,7 +97,7 @@
              ALLGOALS
 	        (action_simp_tac 
                     (simpset() addsimps [WriteInner_def,GoodWrite_def,BadWrite_def,
-					WrRequest_def] delsimps [not1_or])
+					WrRequest_def] delsimps [disj_not1])
                     [] [base_enabled,Pair_inject])
             ]);