simplified tactics slightly

--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Jul 31 00:45:55 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Jul 31 13:19:57 2014 +0200
@@ -223,7 +223,7 @@
     val rel_congs = map rel_cong_of_bnf bnfs;
     val rel_converseps = map rel_conversep_of_bnf bnfs;
     val rel_Grps = map rel_Grp_of_bnf bnfs;
-    val rel_OOs = map rel_OO_of_bnf bnfs;
+    val le_rel_OOs = map le_rel_OO_of_bnf bnfs;
     val in_rels = map in_rel_of_bnf bnfs;
 
     val timer = time (timer "Extracted terms & thms");
@@ -589,7 +589,7 @@
           HOLogic.mk_Trueprop (mk_bis Bs ss B''s s''s (map2 (curry mk_rel_comp) Rs R's));
       in
         Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
-          (K (mk_bis_O_tac lthy m bis_rel_thm rel_congs rel_OOs))
+          (K (mk_bis_O_tac lthy m bis_rel_thm rel_congs le_rel_OOs))
         |> Thm.close_derivation
         |> singleton (Proof_Context.export names_lthy lthy)
       end;
@@ -2260,7 +2260,7 @@
             val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj goals);
           in
             Goal.prove_sorry lthy [] [] goal
-              (K (mk_le_rel_OO_tac Jrel_coinduct_thm dtor_Jrel_thms rel_OOs))
+              (K (mk_le_rel_OO_tac Jrel_coinduct_thm dtor_Jrel_thms le_rel_OOs))
             |> Thm.close_derivation
             |> singleton (Proof_Context.export names_lthy lthy)
           end;

--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Thu Jul 31 00:45:55 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Thu Jul 31 13:19:57 2014 +0200
@@ -277,21 +277,21 @@
         REPEAT_DETERM o etac allE,
         rtac @{thm conversepI}, etac mp, etac @{thm converseD}]) (rel_congs ~~ rel_converseps)] 1;
 
-fun mk_bis_O_tac ctxt m bis_rel rel_congs rel_OOs =
+fun mk_bis_O_tac ctxt m bis_rel rel_congs le_rel_OOs =
   EVERY' [rtac (bis_rel RS iffD2), REPEAT_DETERM o dtac (bis_rel RS iffD1),
     REPEAT_DETERM o etac conjE, rtac conjI,
     CONJ_WRAP' (K (EVERY' [etac @{thm relcomp_subset_Sigma}, atac])) rel_congs,
-    CONJ_WRAP' (fn (rel_cong, rel_OO) =>
+    CONJ_WRAP' (fn (rel_cong, le_rel_OO) =>
       EVERY' [rtac allI, rtac allI, rtac impI,
         rtac (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
         REPEAT_DETERM_N m o rtac @{thm eq_OO},
         REPEAT_DETERM_N (length rel_congs) o rtac @{thm relcompp_in_rel},
-        rtac (rel_OO RS sym RS @{thm eq_refl} RS @{thm predicate2D}),
+        rtac (le_rel_OO RS @{thm predicate2D}),
         etac @{thm relcompE},
         REPEAT_DETERM o dtac prod_injectD,
         etac conjE, hyp_subst_tac ctxt,
         REPEAT_DETERM o etac allE, rtac @{thm relcomppI},
-        etac mp, atac, etac mp, atac]) (rel_congs ~~ rel_OOs)] 1;
+        etac mp, atac, etac mp, atac]) (rel_congs ~~ le_rel_OOs)] 1;
 
 fun mk_bis_Gr_tac ctxt bis_rel rel_Grps mor_images morEs coalg_ins =
   unfold_thms_tac ctxt (bis_rel :: @{thm eq_alt} :: @{thm in_rel_Gr} :: rel_Grps) THEN
@@ -898,14 +898,14 @@
   EVERY' (map rtac [@{thm UNION_Cinfinite_bound}, ordIso_ordLeq_trans, @{thm card_of_nat},
     @{thm natLeq_ordLeq_cinfinite}, sbd_Cinfinite, ballI, col_bd, sbd_Cinfinite]) 1;
 
-fun mk_le_rel_OO_tac coinduct rel_Jrels rel_OOs =
-  EVERY' (rtac coinduct :: map2 (fn rel_Jrel => fn rel_OO =>
+fun mk_le_rel_OO_tac coinduct rel_Jrels le_rel_OOs =
+  EVERY' (rtac coinduct :: map2 (fn rel_Jrel => fn le_rel_OO =>
     let val Jrel_imp_rel = rel_Jrel RS iffD1;
     in
-      EVERY' [rtac (rel_OO RS sym RS @{thm eq_refl} RS @{thm predicate2D}), etac @{thm relcomppE},
+      EVERY' [rtac (le_rel_OO RS @{thm predicate2D}), etac @{thm relcomppE},
       rtac @{thm relcomppI}, etac Jrel_imp_rel, etac Jrel_imp_rel]
     end)
-  rel_Jrels rel_OOs) 1;
+  rel_Jrels le_rel_OOs) 1;
 
 fun mk_wit_tac ctxt n dtor_ctors dtor_set wit coind_wits =
   ALLGOALS (TRY o (eresolve_tac coind_wits THEN' rtac refl)) THEN

--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Jul 31 00:45:55 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Jul 31 13:19:57 2014 +0200
@@ -168,7 +168,7 @@
     val map_ids = map map_id_of_bnf bnfs;
     val set_mapss = map set_map_of_bnf bnfs;
     val rel_mono_strongs = map rel_mono_strong_of_bnf bnfs;
-    val rel_OOs = map rel_OO_of_bnf bnfs;
+    val le_rel_OOs = map le_rel_OO_of_bnf bnfs;
 
     val timer = time (timer "Extracted terms & thms");
 
@@ -1691,7 +1691,7 @@
           in
             Goal.prove_sorry lthy [] [] goal
               (fn {context = ctxt, prems = _} => mk_le_rel_OO_tac ctxt m induct ctor_nchotomy_thms
-                ctor_Irel_thms rel_mono_strongs rel_OOs)
+                ctor_Irel_thms rel_mono_strongs le_rel_OOs)
             |> Thm.close_derivation
             |> singleton (Proof_Context.export names_lthy lthy)
           end;

--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Thu Jul 31 00:45:55 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Thu Jul 31 13:19:57 2014 +0200
@@ -582,17 +582,17 @@
     (induct_tac THEN' EVERY' (map3 mk_map_cong0 ctor_maps map_cong0s set_setsss)) 1
   end;
 
-fun mk_le_rel_OO_tac ctxt m induct ctor_nchotomys ctor_Irels rel_mono_strongs rel_OOs =
+fun mk_le_rel_OO_tac ctxt m induct ctor_nchotomys ctor_Irels rel_mono_strongs le_rel_OOs =
   EVERY' (rtac induct ::
-  map4 (fn nchotomy => fn Irel => fn rel_mono => fn rel_OO =>
+  map4 (fn nchotomy => fn Irel => fn rel_mono => fn le_rel_OO =>
     EVERY' [rtac impI, etac (nchotomy RS @{thm nchotomy_relcomppE}),
       REPEAT_DETERM_N 2 o dtac (Irel RS iffD1), rtac (Irel RS iffD2),
-      rtac rel_mono, rtac (rel_OO RS @{thm predicate2_eqD} RS iffD2),
+      rtac rel_mono, rtac (le_rel_OO RS @{thm predicate2D}),
       rtac @{thm relcomppI}, atac, atac,
       REPEAT_DETERM_N m o EVERY' [rtac ballI, rtac ballI, rtac impI, atac],
-      REPEAT_DETERM_N (length rel_OOs) o
+      REPEAT_DETERM_N (length le_rel_OOs) o
         EVERY' [rtac ballI, rtac ballI, Goal.assume_rule_tac ctxt]])
-  ctor_nchotomys ctor_Irels rel_mono_strongs rel_OOs) 1;
+  ctor_nchotomys ctor_Irels rel_mono_strongs le_rel_OOs) 1;
 
 (* BNF tactics *)