src/FOL/FOL.thy

 
 
 use "simpdata.ML"
 
 simproc_setup defined_Ex ("EX x. P(x)") = {*
-  fn _ => fn ss => fn ct => Quantifier1.rearrange_ex (theory_of_cterm ct) ss (term_of ct)
+  fn _ => fn ss => Quantifier1.rearrange_ex ss o term_of
 *}
 
 simproc_setup defined_All ("ALL x. P(x)") = {*
-  fn _ => fn ss => fn ct => Quantifier1.rearrange_all (theory_of_cterm ct) ss (term_of ct)
+  fn _ => fn ss => Quantifier1.rearrange_all ss o term_of
 *}
 
 ML {*
 (*intuitionistic simprules only*)
 val IFOL_ss =