# HG changeset patch
# User blanchet
# Date 1393955837 -3600
# Node ID 91d5085ad92891f2765b863f6f49438dbd649362
# Parent  0ef30d52c5e4f874c13b0146fed978c4db9d3e90
tuning

diff -r 0ef30d52c5e4 -r 91d5085ad928 src/HOL/Tools/BNF/bnf_comp_tactics.ML
--- 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