diff -r 63e53327f5e5 -r 62d1e642da30 src/HOL/UNITY/Handshake.ML
--- a/src/HOL/UNITY/Handshake.ML	Fri May 21 10:50:04 1999 +0200
+++ b/src/HOL/UNITY/Handshake.ML	Fri May 21 10:56:46 1999 +0200
@@ -27,7 +27,7 @@
 by (rtac (constrains_imp_Constrains RS StableI) 1);
 by (auto_tac (claset(), simpset() addsimps [constrains_Join]));
 by (constrains_tac 2);
-by (auto_tac (claset() addIs [le_anti_sym] addSEs [le_SucE], simpset()));
+by (auto_tac (claset() addIs [order_antisym] addSEs [le_SucE], simpset()));
 by (constrains_tac 1);
 qed "invFG";