# HG changeset patch
# User nipkow
# Date 764518982 -3600
# Node ID 3fb8c0256bec03ae3e907a45f74acdb414824421
# Parent  febeb36a4ba4aea9d7fd30a1bd9c73704ba8e787
removed inconsistency with new HOL version

diff -r febeb36a4ba4 -r 3fb8c0256bec src/HOLCF/Fix.ML
--- 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),
diff -r febeb36a4ba4 -r 3fb8c0256bec src/HOLCF/fix.ML
--- 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),