1.1 --- a/src/HOL/HOL.thy	Fri Apr 22 13:58:13 2011 +0200
     1.2 +++ b/src/HOL/HOL.thy	Fri Apr 22 14:30:32 2011 +0200
     1.3 @@ -1213,11 +1213,11 @@
     1.4  setup {* Simplifier.map_simpset (K HOL_basic_ss) *}
     1.5  
     1.6  simproc_setup defined_Ex ("EX x. P x") = {*
     1.7 -  fn _ => fn ss => fn ct => Quantifier1.rearrange_ex (theory_of_cterm ct) ss (term_of ct)
     1.8 +  fn _ => fn ss => Quantifier1.rearrange_ex ss o term_of
     1.9  *}
    1.10  
    1.11  simproc_setup defined_All ("ALL x. P x") = {*
    1.12 -  fn _ => fn ss => fn ct => Quantifier1.rearrange_all (theory_of_cterm ct) ss (term_of ct)
    1.13 +  fn _ => fn ss => Quantifier1.rearrange_all ss o term_of
    1.14  *}
    1.15  
    1.16  setup {*