--- a/src/HOL/HOL.thy Fri Apr 22 14:53:11 2011 +0200
+++ b/src/HOL/HOL.thy Fri Apr 22 15:05:04 2011 +0200
@@ -1212,13 +1212,8 @@
setup {* Simplifier.map_simpset (K HOL_basic_ss) *}
-simproc_setup defined_Ex ("EX x. P x") = {*
- fn _ => fn ss => Quantifier1.rearrange_ex ss o term_of
-*}
-
-simproc_setup defined_All ("ALL x. P x") = {*
- fn _ => fn ss => Quantifier1.rearrange_all ss o term_of
-*}
+simproc_setup defined_Ex ("EX x. P x") = {* fn _ => Quantifier1.rearrange_ex *}
+simproc_setup defined_All ("ALL x. P x") = {* fn _ => Quantifier1.rearrange_all *}
setup {*
Simplifier.method_setup Splitter.split_modifiers