1.1 --- a/src/ZF/simpdata.ML	Fri Apr 22 13:07:47 2011 +0200
     1.2 +++ b/src/ZF/simpdata.ML	Fri Apr 22 13:58:13 2011 +0200
     1.3 @@ -47,28 +47,5 @@
     1.4    ss setmksimps (K (map mk_eq o ZF_atomize o gen_all))
     1.5    addcongs [@{thm if_weak_cong}]);
     1.6  
     1.7 -local
     1.8 -
     1.9 -val unfold_bex_tac = unfold_tac [@{thm Bex_def}];
    1.10 -fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
    1.11 -val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
    1.12 -
    1.13 -val unfold_ball_tac = unfold_tac [@{thm Ball_def}];
    1.14 -fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
    1.15 -val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
    1.16 -
    1.17 -in
    1.18 -
    1.19 -val defBEX_regroup = Simplifier.simproc_global @{theory}
    1.20 -  "defined BEX" ["EX x:A. P(x) & Q(x)"] rearrange_bex;
    1.21 -
    1.22 -val defBALL_regroup = Simplifier.simproc_global @{theory}
    1.23 -  "defined BALL" ["ALL x:A. P(x) --> Q(x)"] rearrange_ball;
    1.24 -
    1.25 -end;
    1.26 -
    1.27 -Addsimprocs [defBALL_regroup, defBEX_regroup];
    1.28 -
    1.29 -
    1.30  val ZF_ss = @{simpset};
    1.31