diff -r 12a752aeee98 -r 6702c984bf5a src/HOL/Tools/Meson/meson.ML
--- a/src/HOL/Tools/Meson/meson.ML	Fri Apr 22 13:07:47 2011 +0200
+++ b/src/HOL/Tools/Meson/meson.ML	Fri Apr 22 13:58:13 2011 +0200
@@ -567,7 +567,7 @@
 
 val nnf_ss =
   HOL_basic_ss addsimps nnf_extra_simps
-    addsimprocs [defALL_regroup,defEX_regroup, @{simproc neq}, @{simproc let_simp}];
+    addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}, @{simproc neq}, @{simproc let_simp}];
 
 val presimplify =
   rewrite_rule (map safe_mk_meta_eq nnf_simps) #> simplify nnf_ss