--- a/src/HOL/HOL.thy Fri Apr 22 13:07:47 2011 +0200
+++ b/src/HOL/HOL.thy Fri Apr 22 13:58:13 2011 +0200
@@ -1209,8 +1209,15 @@
use "Tools/simpdata.ML"
ML {* open Simpdata *}
-setup {*
- Simplifier.map_simpset (K (HOL_basic_ss addsimprocs [defALL_regroup, defEX_regroup]))
+
+setup {* Simplifier.map_simpset (K HOL_basic_ss) *}
+
+simproc_setup defined_Ex ("EX x. P x") = {*
+ fn _ => fn ss => fn ct => Quantifier1.rearrange_ex (theory_of_cterm ct) ss (term_of ct)
+*}
+
+simproc_setup defined_All ("ALL x. P x") = {*
+ fn _ => fn ss => fn ct => Quantifier1.rearrange_all (theory_of_cterm ct) ss (term_of ct)
*}
setup {*