# HG changeset patch
# User blanchet
# Date 1384977494 -3600
# Node ID 2d23e9c3b66bf93471e740af416a178dbf36888a
# Parent  4626a45bc7799a2f51a1d85aaf5311e1296c7834
killed needless thm

diff -r 4626a45bc779 -r 2d23e9c3b66b src/HOL/BNF/BNF_Util.thy
--- a/src/HOL/BNF/BNF_Util.thy	Wed Nov 20 20:46:46 2013 +0100
+++ b/src/HOL/BNF/BNF_Util.thy	Wed Nov 20 20:58:14 2013 +0100
@@ -41,9 +41,6 @@
 lemma bijI: "\<lbrakk>\<And>x y. (f x = f y) = (x = y); \<And>y. \<exists>x. y = f x\<rbrakk> \<Longrightarrow> bij f"
 unfolding bij_def inj_on_def by auto blast
 
-lemma Collect_pair_mem_eq: "{(x, y). (x, y) \<in> R} = R"
-by simp
-
 (* Operator: *)
 definition "Gr A f = {(a, f a) | a. a \<in> A}"
 
diff -r 4626a45bc779 -r 2d23e9c3b66b src/HOL/BNF/Tools/bnf_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_tactics.ML	Wed Nov 20 20:46:46 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_tactics.ML	Wed Nov 20 20:58:14 2013 +0100
@@ -91,7 +91,7 @@
 fun mk_ctor_or_dtor_rel_tac srel_def IJrel_defs IJsrel_defs dtor_srel {context = ctxt, prems = _} =
   unfold_thms_tac ctxt IJrel_defs THEN
   rtac (unfold_thms ctxt (IJrel_defs @ IJsrel_defs @
-    @{thms Collect_pair_mem_eq mem_Collect_eq fst_conv snd_conv}) dtor_srel RS trans) 1 THEN
+    @{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