src/HOLCF/fix.ML

 	(res_inst_tac [("s","False"),("t","Suc(ia) < Suc(i)")] ssubst 1),
 	(asm_simp_tac nat_ss  1),
 	(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),
 	(hyp_subst_tac 1),
 	(asm_simp_tac nat_ss 1),

 		ssubst 1),
 	(res_inst_tac [("s","False"),("t","n < Suc(i)")] ssubst 1),
 	(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),
 	(rtac mp 1),
 	(atac 1),