# HG changeset patch
# User blanchet
# Date 1392761337 -3600
# Node ID 0d0e19e9505ed166bb1f4f664633b0c8289cab63
# Parent  d7f411651bed54db6f08825558edf92abcff7137
removed deadcode

diff -r d7f411651bed -r 0d0e19e9505e src/HOL/Tools/BNF/bnf_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_tactics.ML	Tue Feb 18 23:08:55 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_tactics.ML	Tue Feb 18 23:08:57 2014 +0100
@@ -12,7 +12,6 @@
 
   val fo_rtac: thm -> Proof.context -> int -> tactic
 
-  val mk_flatten_assoc_tac: (int -> tactic) -> thm -> thm -> thm -> tactic
   val mk_rotate_eq_tac: (int -> tactic) -> thm -> thm -> thm -> thm -> ''a list -> ''a list ->
     int -> tactic
 
@@ -21,8 +20,6 @@
   val mk_Abs_bij_thm: Proof.context -> thm -> thm -> thm
   val mk_Abs_inj_thm: thm -> thm
 
-  val mk_ctor_or_dtor_rel_tac: Proof.context -> thm -> thm list -> thm list -> thm -> tactic
-
   val mk_map_comp_id_tac: thm -> tactic
   val mk_map_cong0_tac: Proof.context -> int -> thm -> tactic
   val mk_map_cong0L_tac: int -> thm -> thm -> tactic
@@ -85,15 +82,6 @@
     gen_tac
   end;
 
-fun mk_ctor_or_dtor_rel_tac ctxt srel_def IJrel_defs IJsrel_defs dtor_srel =
-  unfold_thms_tac ctxt IJrel_defs THEN
-  rtac (unfold_thms ctxt (IJrel_defs @ IJsrel_defs @
-    @{thms Collect_mem_eq mem_Collect_eq fst_conv snd_conv}) dtor_srel RS trans) 1 THEN
-  unfold_thms_tac ctxt (srel_def ::
-    @{thms pair_collapse Collect_mem_eq mem_Collect_eq prod.cases fst_conv snd_conv
-      split_conv}) THEN
-  rtac refl 1;
-
 fun mk_map_comp_id_tac map_comp0 =
   (rtac trans THEN' rtac map_comp0 THEN' REPEAT_DETERM o stac @{thm comp_id} THEN' rtac refl) 1;