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