diff -r 548a34929e98 -r 603320b93668 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Nov 12 17:21:43 2009 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Nov 12 17:21:48 2009 +0100
@@ -1233,7 +1233,7 @@
   also have "\<dots> = (\<exists>x. (Ifm vs (y#bs) ?cyes) \<and> (Ifm vs (x#bs) ?cno))"
     using bound0_I[OF yes_nb, where bs="bs" and b'="y"] by blast
   also have "\<dots> = (Ifm vs bs (decr0 ?cyes) \<and> Ifm vs bs (E ?cno))"
-    by (auto simp add: decr0[OF yes_nb])
+    by (auto simp add: decr0[OF yes_nb] simp del: partition_filter_conv)
   also have "\<dots> = (Ifm vs bs (conj (decr0 ?cyes) (qe ?cno)))"
     using qe[rule_format, OF no_qf] by auto
   finally have "Ifm vs bs (E p) = Ifm vs bs (CJNB qe p)"