1.1 --- a/src/HOLCF/Fix.ML	Thu Mar 24 13:45:06 1994 +0100
     1.2 +++ b/src/HOLCF/Fix.ML	Thu Mar 24 15:23:02 1994 +0100
     1.3 @@ -894,7 +894,7 @@
     1.4  	(rtac iffI 1),
     1.5  	(etac FalseE 2),
     1.6  	(rtac notE 1),
     1.7 -	(etac (less_not_sym RS mp) 1),	
     1.8 +	(etac less_not_sym 1),	
     1.9  	(atac 1),
    1.10  	(asm_simp_tac Cfun_ss  1),
    1.11  	(etac (is_chainE RS spec) 1),
    1.12 @@ -934,7 +934,7 @@
    1.13  	(rtac iffI 1),
    1.14  	(etac FalseE 2),
    1.15  	(rtac notE 1),
    1.16 -	(etac (less_not_sym RS mp) 1),	
    1.17 +	(etac less_not_sym 1),	
    1.18  	(atac 1),
    1.19  	(asm_simp_tac nat_ss 1),
    1.20  	(dtac spec 1),

     2.1 --- a/src/HOLCF/fix.ML	Thu Mar 24 13:45:06 1994 +0100
     2.2 +++ b/src/HOLCF/fix.ML	Thu Mar 24 15:23:02 1994 +0100
     2.3 @@ -894,7 +894,7 @@
     2.4  	(rtac iffI 1),
     2.5  	(etac FalseE 2),
     2.6  	(rtac notE 1),
     2.7 -	(etac (less_not_sym RS mp) 1),	
     2.8 +	(etac less_not_sym 1),	
     2.9  	(atac 1),
    2.10  	(asm_simp_tac Cfun_ss  1),
    2.11  	(etac (is_chainE RS spec) 1),
    2.12 @@ -934,7 +934,7 @@
    2.13  	(rtac iffI 1),
    2.14  	(etac FalseE 2),
    2.15  	(rtac notE 1),
    2.16 -	(etac (less_not_sym RS mp) 1),	
    2.17 +	(etac less_not_sym 1),	
    2.18  	(atac 1),
    2.19  	(asm_simp_tac nat_ss 1),
    2.20  	(dtac spec 1),