src/ZF/pair.thy
changeset 42456 13b4b6ba3593
parent 42455 6702c984bf5a
child 42459 38b9f023cc34
     1.1 --- a/src/ZF/pair.thy	Fri Apr 22 13:58:13 2011 +0200
     1.2 +++ b/src/ZF/pair.thy	Fri Apr 22 14:30:32 2011 +0200
     1.3 @@ -15,8 +15,7 @@
     1.4      val unfold_bex_tac = unfold_tac @{thms Bex_def};
     1.5      fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
     1.6    in
     1.7 -    fn _ => fn ss => fn ct =>
     1.8 -      Quantifier1.rearrange_bex prove_bex_tac (theory_of_cterm ct) ss (term_of ct)
     1.9 +    fn _ => fn ss => Quantifier1.rearrange_bex (prove_bex_tac ss) ss o term_of
    1.10    end
    1.11  *}
    1.12  
    1.13 @@ -25,8 +24,7 @@
    1.14      val unfold_ball_tac = unfold_tac @{thms Ball_def};
    1.15      fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
    1.16    in
    1.17 -    fn _ => fn ss => fn ct =>
    1.18 -      Quantifier1.rearrange_ball prove_ball_tac (theory_of_cterm ct) ss (term_of ct)
    1.19 +    fn _ => fn ss => Quantifier1.rearrange_ball (prove_ball_tac ss) ss o term_of
    1.20    end
    1.21  *}
    1.22