--- 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}"
--- 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