src/HOL/HOL.thy

--- a/src/HOL/HOL.thy	Fri Apr 22 00:57:59 2011 +0200
+++ b/src/HOL/HOL.thy	Fri Apr 22 12:46:48 2011 +0200
@@ -1209,10 +1209,12 @@
 
 use "Tools/simpdata.ML"
 ML {* open Simpdata *}
+setup {*
+  Simplifier.map_simpset (K (HOL_basic_ss addsimprocs [defALL_regroup, defEX_regroup]))
+*}
 
 setup {*
   Simplifier.method_setup Splitter.split_modifiers
-  #> Simplifier.map_simpset (K Simpdata.simpset_simprocs)
   #> Splitter.setup
   #> clasimp_setup
   #> EqSubst.setup