1.1 --- a/src/HOL/HOL.thy	Fri Apr 22 13:07:47 2011 +0200
     1.2 +++ b/src/HOL/HOL.thy	Fri Apr 22 13:58:13 2011 +0200
     1.3 @@ -1209,8 +1209,15 @@
     1.4  
     1.5  use "Tools/simpdata.ML"
     1.6  ML {* open Simpdata *}
     1.7 -setup {*
     1.8 -  Simplifier.map_simpset (K (HOL_basic_ss addsimprocs [defALL_regroup, defEX_regroup]))
     1.9 +
    1.10 +setup {* Simplifier.map_simpset (K HOL_basic_ss) *}
    1.11 +
    1.12 +simproc_setup defined_Ex ("EX x. P x") = {*
    1.13 +  fn _ => fn ss => fn ct => Quantifier1.rearrange_ex (theory_of_cterm ct) ss (term_of ct)
    1.14 +*}
    1.15 +
    1.16 +simproc_setup defined_All ("ALL x. P x") = {*
    1.17 +  fn _ => fn ss => fn ct => Quantifier1.rearrange_all (theory_of_cterm ct) ss (term_of ct)
    1.18  *}
    1.19  
    1.20  setup {*