# HG changeset patch
# User blanchet
# Date 1277393147 -7200
# Node ID c80e77e8d0369b66639aca19f6daae7ede7769ae
# Parent  97ab019d5ac8f30b2f9bfeef69738f2355c8c834
cosmetics

diff -r 97ab019d5ac8 -r c80e77e8d036 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Thu Jun 24 10:38:01 2010 +0200
+++ b/src/HOL/Tools/meson.ML	Thu Jun 24 17:25:47 2010 +0200
@@ -521,10 +521,9 @@
   nnf_ss also includes the one-point simprocs,
   which are needed to avoid the various one-point theorems from generating junk clauses.*)
 val nnf_simps =
-  [@{thm simp_implies_def}, @{thm Ex1_def}, @{thm Ball_def},@{thm  Bex_def}, @{thm if_True},
-    @{thm if_False}, @{thm if_cancel}, @{thm if_eq_cancel}, @{thm cases_simp}];
-val nnf_extra_simps =
-  @{thms split_ifs} @ @{thms ex_simps} @ @{thms all_simps} @ @{thms simp_thms};
+  @{thms simp_implies_def Ex1_def Ball_def Bex_def if_True if_False if_cancel
+         if_eq_cancel cases_simp}
+val nnf_extra_simps = @{thms split_ifs ex_simps all_simps simp_thms}
 
 val nnf_ss =
   HOL_basic_ss addsimps nnf_extra_simps