--- a/src/HOLCF/Fix.ML Thu Mar 24 13:45:06 1994 +0100
+++ b/src/HOLCF/Fix.ML Thu Mar 24 15:23:02 1994 +0100
@@ -894,7 +894,7 @@
(rtac iffI 1),
(etac FalseE 2),
(rtac notE 1),
- (etac (less_not_sym RS mp) 1),
+ (etac less_not_sym 1),
(atac 1),
(asm_simp_tac Cfun_ss 1),
(etac (is_chainE RS spec) 1),
@@ -934,7 +934,7 @@
(rtac iffI 1),
(etac FalseE 2),
(rtac notE 1),
- (etac (less_not_sym RS mp) 1),
+ (etac less_not_sym 1),
(atac 1),
(asm_simp_tac nat_ss 1),
(dtac spec 1),
--- a/src/HOLCF/fix.ML Thu Mar 24 13:45:06 1994 +0100
+++ b/src/HOLCF/fix.ML Thu Mar 24 15:23:02 1994 +0100
@@ -894,7 +894,7 @@
(rtac iffI 1),
(etac FalseE 2),
(rtac notE 1),
- (etac (less_not_sym RS mp) 1),
+ (etac less_not_sym 1),
(atac 1),
(asm_simp_tac Cfun_ss 1),
(etac (is_chainE RS spec) 1),
@@ -934,7 +934,7 @@
(rtac iffI 1),
(etac FalseE 2),
(rtac notE 1),
- (etac (less_not_sym RS mp) 1),
+ (etac less_not_sym 1),
(atac 1),
(asm_simp_tac nat_ss 1),
(dtac spec 1),