src/FOL/FOL.thy
changeset 42456 13b4b6ba3593
parent 42455 6702c984bf5a
child 42459 38b9f023cc34
     1.1 --- a/src/FOL/FOL.thy	Fri Apr 22 13:58:13 2011 +0200
     1.2 +++ b/src/FOL/FOL.thy	Fri Apr 22 14:30:32 2011 +0200
     1.3 @@ -307,11 +307,11 @@
     1.4  use "simpdata.ML"
     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  ML {*