tidied

--- a/src/HOL/UNITY/Mutex.ML	Wed Mar 08 16:15:41 2000 +0100
+++ b/src/HOL/UNITY/Mutex.ML	Wed Mar 08 16:17:10 2000 +0100
@@ -26,8 +26,7 @@
 
 (*The safety property: mutual exclusion*)
 Goal "Mutex : Always {s. ~ (m s = #3 & n s = #3)}";
-by (rtac Always_weaken 1);
-by (rtac ([IU, IV] MRS Always_Int_I) 1);
+by (rtac ([IU, IV] MRS Always_Int_I RS Always_weaken) 1);
 by Auto_tac;
 qed "mutual_exclusion";