--- a/src/HOL/Tools/simpdata.ML Fri Apr 22 13:07:47 2011 +0200
+++ b/src/HOL/Tools/simpdata.ML Fri Apr 22 13:58:13 2011 +0200
@@ -183,14 +183,6 @@
let val ss0 = Simplifier.clear_ss HOL_basic_ss addsimps ths
in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end;
-val defALL_regroup =
- Simplifier.simproc_global @{theory}
- "defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all;
-
-val defEX_regroup =
- Simplifier.simproc_global @{theory}
- "defined EX" ["EX x. P x"] Quantifier1.rearrange_ex;
-
end;
structure Splitter = Simpdata.Splitter;