# [isabelle] Product_Type.split_beta fails

Hi all,
I'm getting exceptions from the split_beta simproc which propagate to
the "user-level" (Isabelle 2013). Here's a minimal example:
lemma "P (\<lambda>s. (case s of (x, y) \<Rightarrow> c))"
using [[simp_depth_limit=0]]
apply(simp)
This results in:
*** Proof failed.
*** (case :000 of (x, y) \<Rightarrow> c) = c
*** 1. (case :000 of (x, y) \<Rightarrow> c) = c
*** The error(s) above occurred for the goal statement:
*** (case :000 of (x, y) \<Rightarrow> c) = c
Setting the depth limit to 2 or higher makes the error go away. Glancing
at the simproc, it seems that its local function "meta_eq" assumes that
rewriting with just "cond_split_eta" will work, but this fails at low
simp depths.
Cheers,
Ognjen

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*