src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
changeset 61424 c3658c18b7bc
parent 61334 8d40ddaa427f
child 61551 078c9fd2e052
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -66,7 +66,7 @@
     1.4    | unfold_lets_splits (t $ u) = betapply (unfold_lets_splits t, unfold_lets_splits u)
     1.5    | unfold_lets_splits (Abs (s, T, t)) = Abs (s, T, unfold_lets_splits t)
     1.6    | unfold_lets_splits t = t
     1.7 -and unfold_splits_lets ((t as Const (@{const_name uncurry}, _)) $ u) =
     1.8 +and unfold_splits_lets ((t as Const (@{const_name case_prod}, _)) $ u) =
     1.9      (case unfold_splits_lets u of
    1.10        u' as Abs (s1, T1, Abs (s2, T2, _)) =>
    1.11        let val v = Var ((s1 ^ s2, Term.maxidx_of_term u' + 1), HOLogic.mk_prodT (T1, T2)) in