src/HOL/Set.thy
 changeset 42456 13b4b6ba3593 parent 42455 6702c984bf5a child 42459 38b9f023cc34
```     1.1 --- a/src/HOL/Set.thy	Fri Apr 22 13:58:13 2011 +0200
1.2 +++ b/src/HOL/Set.thy	Fri Apr 22 14:30:32 2011 +0200
1.3 @@ -77,13 +77,12 @@
1.4
1.5  simproc_setup defined_Collect ("{x. P x & Q x}") = {*
1.6    let
1.7 -    val Coll_perm_tac =
1.8 +    val Collect_perm_tac =
1.9        rtac @{thm Collect_cong} 1 THEN
1.10        rtac @{thm iffI} 1 THEN
1.11        ALLGOALS (EVERY' [REPEAT_DETERM o etac @{thm conjE}, DEPTH_SOLVE_1 o ares_tac @{thms conjI}]);
1.12    in
1.13 -    fn _ => fn ss => fn ct =>
1.14 -      Quantifier1.rearrange_Coll Coll_perm_tac (theory_of_cterm ct) ss (term_of ct)
1.15 +    fn _ => fn ss => Quantifier1.rearrange_Collect Collect_perm_tac ss o term_of
1.16    end
1.17  *}
1.18
1.19 @@ -333,8 +332,7 @@
1.20      val unfold_bex_tac = unfold_tac @{thms Bex_def};
1.21      fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
1.22    in
1.23 -    fn _ => fn ss => fn ct =>
1.24 -      Quantifier1.rearrange_bex prove_bex_tac (theory_of_cterm ct) ss (term_of ct)
1.25 +    fn _ => fn ss => Quantifier1.rearrange_bex (prove_bex_tac ss) ss o term_of
1.26    end
1.27  *}
1.28
1.29 @@ -343,8 +341,7 @@
1.30      val unfold_ball_tac = unfold_tac @{thms Ball_def};
1.31      fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
1.32    in
1.33 -    fn _ => fn ss => fn ct =>
1.34 -      Quantifier1.rearrange_ball prove_ball_tac (theory_of_cterm ct) ss (term_of ct)
1.35 +    fn _ => fn ss => Quantifier1.rearrange_ball (prove_ball_tac ss) ss o term_of
1.36    end
1.37  *}
1.38
```