diff -r a16ee2b38db2 -r 694d0c88d86a src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Tue Aug 31 08:00:53 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Tue Aug 31 08:00:54 2010 +0200
@@ -259,7 +259,8 @@
 
 fun rewrite_intros thy =
   Simplifier.full_simplify (HOL_basic_ss addsimps [@{thm all_not_ex}])
-  #> Simplifier.full_simplify (HOL_basic_ss addsimps @{thms bool_simps} addsimps @{thms nnf_simps})
+  #> Simplifier.full_simplify
+    (HOL_basic_ss addsimps (tl @{thms bool_simps}) addsimps @{thms nnf_simps})
   #> map_term thy (maps_premises (split_conjs thy))
 
 fun print_specs options thy msg ths =