src/FOL/FOL.thy
changeset 42459 38b9f023cc34
parent 42456 13b4b6ba3593
child 42477 52fa26b6c524
     1.1 --- a/src/FOL/FOL.thy	Fri Apr 22 14:53:11 2011 +0200
     1.2 +++ b/src/FOL/FOL.thy	Fri Apr 22 15:05:04 2011 +0200
     1.3 @@ -306,13 +306,8 @@
     1.4  
     1.5  use "simpdata.ML"
     1.6  
     1.7 -simproc_setup defined_Ex ("EX x. P(x)") = {*
     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 => Quantifier1.rearrange_all ss o term_of
    1.13 -*}
    1.14 +simproc_setup defined_Ex ("EX x. P(x)") = {* fn _ => Quantifier1.rearrange_ex *}
    1.15 +simproc_setup defined_All ("ALL x. P(x)") = {* fn _ => Quantifier1.rearrange_all *}
    1.16  
    1.17  ML {*
    1.18  (*intuitionistic simprules only*)