src/HOL/HOL.thy
changeset 42459 38b9f023cc34
parent 42456 13b4b6ba3593
child 42477 52fa26b6c524
     1.1 --- a/src/HOL/HOL.thy	Fri Apr 22 14:53:11 2011 +0200
     1.2 +++ b/src/HOL/HOL.thy	Fri Apr 22 15:05:04 2011 +0200
     1.3 @@ -1212,13 +1212,8 @@
     1.4  
     1.5  setup {* Simplifier.map_simpset (K HOL_basic_ss) *}
     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  setup {*
    1.18    Simplifier.method_setup Splitter.split_modifiers