src/HOL/HOL.thy
changeset 42456 13b4b6ba3593
parent 42455 6702c984bf5a
child 42459 38b9f023cc34
--- a/src/HOL/HOL.thy	Fri Apr 22 13:58:13 2011 +0200
+++ b/src/HOL/HOL.thy	Fri Apr 22 14:30:32 2011 +0200
@@ -1213,11 +1213,11 @@
 setup {* Simplifier.map_simpset (K HOL_basic_ss) *}
 
 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
 *}
 
 setup {*