--- a/src/HOL/ATP.thy Tue Sep 02 14:40:32 2014 +0200
+++ b/src/HOL/ATP.thy Tue Sep 02 16:38:26 2014 +0200
@@ -135,7 +135,7 @@
(* Has all needed simplification lemmas for logic.
"HOL.simp_thms(35-42)" are about \<exists> and \<forall>. These lemmas are left out for now. *)
-lemmas waldmeister_fol = simp_thms(1-34) disj_absorb disj_left_absorb conj_absorb conj_left_absorb
+lemmas waldmeister_fol = simp_thms(1,2,4-8,11-34) disj_absorb disj_left_absorb conj_absorb conj_left_absorb
eq_ac disj_comms disj_assoc conj_comms conj_assoc