--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Sun Sep 06 22:14:51 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Sun Sep 06 22:14:51 2015 +0200
@@ -66,7 +66,7 @@
| unfold_lets_splits (t $ u) = betapply (unfold_lets_splits t, unfold_lets_splits u)
| unfold_lets_splits (Abs (s, T, t)) = Abs (s, T, unfold_lets_splits t)
| unfold_lets_splits t = t
-and unfold_splits_lets ((t as Const (@{const_name case_prod}, _)) $ u) =
+and unfold_splits_lets ((t as Const (@{const_name uncurry}, _)) $ u) =
(case unfold_splits_lets u of
u' as Abs (s1, T1, Abs (s2, T2, _)) =>
let val v = Var ((s1 ^ s2, Term.maxidx_of_term u' + 1), HOLogic.mk_prodT (T1, T2)) in