make tactic actually work for op = as relator

--- a/src/HOL/BNF/Tools/bnf_def.ML	Wed May 08 06:14:11 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Wed May 08 09:39:30 2013 +0200
@@ -1075,7 +1075,7 @@
             val goal =
               fold_rev Logic.all (x :: y :: Rs) (mk_Trueprop_eq (lhs, rhs));
           in
-            Goal.prove_sorry lthy [] [] goal (mk_in_rel_tac rel_OO_Grps)
+            Goal.prove_sorry lthy [] [] goal (mk_in_rel_tac (the_single rel_OO_Grps))
             |> Thm.close_derivation
           end;
 

--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML	Wed May 08 06:14:11 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML	Wed May 08 09:39:30 2013 +0200
@@ -21,7 +21,7 @@
   val mk_rel_eq_tac: int -> thm -> thm -> thm -> tactic
   val mk_rel_OO_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
     {prems: thm list, context: Proof.context} -> tactic
-  val mk_in_rel_tac: thm list -> {prems: 'b, context: Proof.context} -> tactic
+  val mk_in_rel_tac: thm -> {prems: 'a, context: Proof.context} -> tactic
   val mk_rel_conversep_tac: thm -> thm -> tactic
   val mk_rel_conversep_le_tac: thm list -> thm -> thm -> thm -> thm list ->
     {prems: thm list, context: Proof.context} -> tactic
@@ -185,9 +185,8 @@
           rtac (map_comp RS sym), atac, atac]) [@{thm fst_fstOp}, @{thm snd_sndOp}])] 1
   end;
 
-fun mk_in_rel_tac rel_OO_Grs {context = ctxt, prems = _} =
-  unfold_thms_tac ctxt rel_OO_Grs THEN
-  EVERY' [rtac iffI,
+fun mk_in_rel_tac rel_OO_Gr {context = ctxt, prems = _} =
+  EVERY' [rtac (rel_OO_Gr RS fun_cong RS fun_cong RS trans), rtac iffI,
     REPEAT_DETERM o eresolve_tac [@{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
     hyp_subst_tac ctxt, rtac exI, rtac conjI, atac, rtac conjI, rtac refl, rtac refl,
     REPEAT_DETERM o eresolve_tac [exE, conjE], rtac @{thm relcomppI}, rtac @{thm conversepI},