# HG changeset patch
# User paulson
# Date 937817176 -7200
# Node ID abefbd41bd3e6dc7ce9a80068fe3c05f02110977
# Parent  b6599e2920112081777ae5dafc0c2d512f436d1b
renamed Always_Int to Always_Int_I

diff -r b6599e292011 -r abefbd41bd3e src/HOL/UNITY/Mutex.ML
--- a/src/HOL/UNITY/Mutex.ML	Mon Sep 20 10:45:30 1999 +0200
+++ b/src/HOL/UNITY/Mutex.ML	Mon Sep 20 10:46:16 1999 +0200
@@ -27,7 +27,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) 1);
+by (rtac ([IU, IV] MRS Always_Int_I) 1);
 by Auto_tac;
 qed "mutual_exclusion";