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}