--- a/src/HOL/Tools/BNF/bnf_comp_tactics.ML Tue Mar 04 18:57:17 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp_tactics.ML Tue Mar 04 18:57:17 2014 +0100
@@ -130,7 +130,7 @@
fun gen_after _ = rtac @{thm ordIso_imp_ordLeq} THEN' rtac @{thm cprod_csum_distrib1};
in
(case bd_ordIso_natLeq_opt of
- SOME thm => rtac (thm RS rotate_prems 1 @{thm ordLeq_ordIso_trans}) 1
+ SOME thm => rtac (thm RSN (2, @{thm ordLeq_ordIso_trans})) 1
| NONE => all_tac) THEN
unfold_thms_tac ctxt [comp_set_alt] THEN
rtac @{thm comp_set_bd_Union_o_collect} 1 THEN