--- a/src/HOL/BNF/BNF_Util.thy Wed Nov 20 20:58:14 2013 +0100
+++ b/src/HOL/BNF/BNF_Util.thy Wed Nov 20 21:28:58 2013 +0100
@@ -26,12 +26,6 @@
(\<forall> b1 b2. b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2 \<longrightarrow>
(\<exists> a \<in> A. e1 (p1 a) = e1 b1 \<and> e2 (p2 a) = e2 b2))"
-lemma fst_snd: "\<lbrakk>snd x = (y, z)\<rbrakk> \<Longrightarrow> fst (snd x) = y"
-by simp
-
-lemma snd_snd: "\<lbrakk>snd x = (y, z)\<rbrakk> \<Longrightarrow> snd (snd x) = z"
-by simp
-
lemma fstI: "x = (y, z) \<Longrightarrow> fst x = y"
by simp
--- a/src/HOL/BNF/Tools/bnf_util.ML Wed Nov 20 20:58:14 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_util.ML Wed Nov 20 21:28:58 2013 +0100
@@ -510,7 +510,7 @@
fun mk_nth_conv n m =
let
- fun thm b = if b then @{thm fst_snd} else @{thm snd_snd}
+ fun thm b = if b then @{thm fstI} else @{thm sndI}
fun mk_nth_conv _ 1 1 = refl
| mk_nth_conv _ _ 1 = @{thm fst_conv}
| mk_nth_conv _ 2 2 = @{thm snd_conv}