diff -r 970ee38495e4 -r 3003ddbd46d9 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Thu Aug 19 14:39:31 2010 +0200
+++ b/src/HOL/Tools/meson.ML	Thu Aug 19 18:16:47 2010 +0200
@@ -527,7 +527,8 @@
   which are needed to avoid the various one-point theorems from generating junk clauses.*)
 val nnf_simps =
   @{thms simp_implies_def Ex1_def Ball_def Bex_def if_True if_False if_cancel
-         if_eq_cancel cases_simp}
+         if_eq_cancel cases_simp (* TODO: mem_def_raw Collect_def_raw *)}
+(* TODO:  @ [@{lemma "{} = (%x. False)" by (rule ext) auto}] *)
 val nnf_extra_simps = @{thms split_ifs ex_simps all_simps simp_thms}
 
 val nnf_ss =
@@ -539,8 +540,7 @@
   #> simplify nnf_ss
 
 fun make_nnf ctxt th = case prems_of th of
-    [] => th |> presimplify
-             |> make_nnf1 ctxt
+    [] => th |> presimplify |> make_nnf1 ctxt
   | _ => raise THM ("make_nnf: premises in argument", 0, [th]);
 
 (*Pull existential quantifiers to front. This accomplishes Skolemization for