# HG changeset patch
# User traytel
# Date 1367998770 -7200
# Node ID 87767611de372c6135d12bf313f4141e4c4a4034
# Parent  df962fe09a37ed6f8bd2725e6c85b76624c87fad
make tactic actually work for op = as relator

diff -r df962fe09a37 -r 87767611de37 src/HOL/BNF/Tools/bnf_def.ML
--- 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;
 
diff -r df962fe09a37 -r 87767611de37 src/HOL/BNF/Tools/bnf_def_tactics.ML
--- 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},