src/HOL/UNITY/Union.ML

--- a/src/HOL/UNITY/Union.ML	Tue Feb 29 10:41:08 2000 +0100
+++ b/src/HOL/UNITY/Union.ML	Tue Feb 29 10:57:30 2000 +0100
@@ -147,7 +147,8 @@
 qed "JN_Un";
 
 Goal "(JN i:I. c) = (if I={} then SKIP else c)";
-by (auto_tac (claset() addSIs [program_equalityI], simpset()));
+by (rtac program_equalityI 1);
+by Auto_tac;
 qed "JN_constant";
 
 Goal "(JN i:I. F i Join G i) = (JN i:I. F i)  Join  (JN i:I. G i)";