src/HOL/UNITY/Handshake.ML
changeset 9403 aad13b59b8d9
parent 7523 3a716ebc2fc0
--- a/src/HOL/UNITY/Handshake.ML	Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/Handshake.ML	Fri Jul 21 18:01:36 2000 +0200
@@ -19,7 +19,7 @@
 by (rtac AlwaysI 1);
 by (Force_tac 1);
 by (rtac (constrains_imp_Constrains RS StableI) 1);
-by (auto_tac (claset(), simpset() addsimps [Join_constrains]));
+by Auto_tac;
 by (constrains_tac 2);
 by (auto_tac (claset() addIs [order_antisym] addSEs [le_SucE], simpset()));
 by (constrains_tac 1);