# HG changeset patch
# User blanchet
# Date 1384979338 -3600
# Node ID 7d23f8e501d4bcdab690a7f949023700a16d0c49
# Parent  2d23e9c3b66bf93471e740af416a178dbf36888a
killed more needless thms

diff -r 2d23e9c3b66b -r 7d23f8e501d4 src/HOL/BNF/BNF_Util.thy
--- 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
 
diff -r 2d23e9c3b66b -r 7d23f8e501d4 src/HOL/BNF/Tools/bnf_util.ML
--- 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}