# [isabelle] Set_Comprehension_Pointfree simproc produces unexpected "tactic failed" exception

```Refering to RC-2:

Here is a minimal example:

lemma "finite {(q, q', _). R q \<and>  P q' q}"
apply simp
*** Tactic failed
*** The error(s) above occurred for the goal statement:
*** {(q, ab). R q \<and> (case ab of (q', uu_) \<Rightarrow> P q' q)} =
*** {(q, ab) |q ab. R q \<and> (case ab of (q', uu_) \<Rightarrow> P q'
q)}
***  (line 7 of "/home/lammich/devel/isabelle/Scratch.thy")
*** At command "apply" (line 7 of
"/home/lammich/devel/isabelle/Scratch.thy")

Exception trace - Tactic failed
The error(s) above occurred for the goal statement:
{(q, ab). R q \<and> (case ab of (q', uu_) \<Rightarrow> P q' q)} =
{(q, ab) |q ab. R q \<and> (case ab of (q', uu_) \<Rightarrow> P q' q)}
(line 7 of "/home/lammich/devel/isabelle/Scratch.thy")
Goal.prove_common(7)
Set_Comprehension_Pointfree.comprehension_conv(2)
Conv.then_conv(3)
Set_Comprehension_Pointfree.conv(2)
Set_Comprehension_Pointfree.simproc(2)
Raw_Simplifier.rewritec(4)proc_rews(1)
Raw_Simplifier.rewritec(4)
Raw_Simplifier.bottomc(3)botc(3)
Raw_Simplifier.bottomc(3)subc(3)appc(1)
Raw_Simplifier.bottomc(3)subc(3)
Raw_Simplifier.bottomc(3)botc(3)
Raw_Simplifier.bottomc(3)try_botc(1)(1)
Conv.gconv_rule(3)
Tactical.THEN(1)(1)
Seq.maps(2)(1)
Seq.maps(2)(1)
Seq.filter(2)copy(1)(1)
Seq.append(2)copy(1)(1)
Seq.append(2)copy(1)(1)
Seq.map(2)(1)
Seq.map(2)(1)
Seq.map(2)(1)
Seq.map(2)(1)
Seq.append(2)copy(1)(1)
Seq.first_result(2)result(2)
Seq.first_result(2)
Toplevel.proofs'(1)(1)(1)

```

• Follow-Ups:

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