src/HOL/BNF/Tools/bnf_def_tactics.ML

   val mk_map_wppull_tac: thm -> thm -> thm -> thm -> thm list -> tactic
   val mk_set_map': thm -> thm
 
   val mk_rel_Grp_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
     {prems: thm list, context: Proof.context} -> tactic
-  val mk_rel_eq_tac: int -> thm -> thm -> thm -> {prems: 'a, context: Proof.context} -> tactic
+  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_rel_conversep_tac: thm -> thm -> tactic
   val mk_rel_conversep_le_tac: thm list -> thm -> thm -> thm -> thm list ->

                 rtac @{thm convol_mem_GrpI[OF refl]}, etac set_mp, atac])
             set_maps])
           @{thms fst_convol snd_convol} [map_id', refl])] 1
   end;
 
-fun mk_rel_eq_tac n rel_Grp rel_cong map_id {context = ctxt, prems = _} =
+fun mk_rel_eq_tac n rel_Grp rel_cong map_id =
   (EVERY' (rtac (rel_cong RS trans) :: replicate n (rtac @{thm eq_alt})) THEN'
   rtac (rel_Grp RSN (2, @{thm box_equals[OF _ sym sym[OF eq_alt]]})) THEN'
   (if n = 0 then rtac refl
   else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ "Grp"]},
     rtac @{thm equalityI}, rtac subset_UNIV, rtac subsetI, rtac CollectI,