diff -r 12a752aeee98 -r 6702c984bf5a src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Fri Apr 22 13:07:47 2011 +0200
+++ b/src/FOL/simpdata.ML	Fri Apr 22 13:58:13 2011 +0200
@@ -80,14 +80,6 @@
   val ex_comm = @{thm ex_comm}
 end);
 
-val defEX_regroup =
-  Simplifier.simproc_global @{theory}
-    "defined EX" ["EX x. P(x)"] Quantifier1.rearrange_ex;
-
-val defALL_regroup =
-  Simplifier.simproc_global @{theory}
-    "defined ALL" ["ALL x. P(x)"] Quantifier1.rearrange_all;
-
 
 (*** Case splitting ***)