diff -r 191d9384966a -r d4859efc1096 src/HOL/BNF/Tools/bnf_lfp_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Fri Sep 21 18:25:17 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Fri Sep 21 18:25:17 2012 +0200
@@ -23,6 +23,8 @@
   val mk_ctor_induct2_tac: ctyp option list -> cterm option list -> thm -> thm list ->
     {prems: 'a, context: Proof.context} -> tactic
   val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list -> tactic
+  val mk_dtor_srel_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm ->
+    thm list -> thm list -> thm list list -> tactic
   val mk_ex_copy_alg_tac: int -> thm -> thm -> tactic
   val mk_in_bd_tac: thm -> thm -> thm -> thm -> tactic
   val mk_incl_min_alg_tac: (int -> tactic) -> thm list list list -> thm list -> thm ->
@@ -69,8 +71,6 @@
   val mk_set_natural_tac: thm -> tactic
   val mk_set_simp_tac: thm -> thm -> thm list -> tactic
   val mk_set_tac: thm -> tactic
-  val mk_srel_simp_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm ->
-    thm -> thm list -> thm list -> thm list list -> tactic
   val mk_wit_tac: int -> thm list -> thm list -> tactic
   val mk_wpull_tac: thm -> tactic
 end;
@@ -770,7 +770,7 @@
           EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp,
             REPEAT_DETERM_N n o etac UnE]))))] 1);
 
-fun mk_srel_simp_tac in_Isrels i in_srel map_comp map_cong map_simp set_simps ctor_inject
+fun mk_dtor_srel_tac in_Isrels i in_srel map_comp map_cong map_simp set_simps ctor_inject
   ctor_dtor set_naturals set_incls set_set_inclss =
   let
     val m = length set_incls;