src/ZF/OrdQuant.thy
changeset 42459 38b9f023cc34
parent 42456 13b4b6ba3593
child 45625 750c5a47400b
     1.1 --- a/src/ZF/OrdQuant.thy	Fri Apr 22 14:53:11 2011 +0200
     1.2 +++ b/src/ZF/OrdQuant.thy	Fri Apr 22 15:05:04 2011 +0200
     1.3 @@ -372,18 +372,14 @@
     1.4    let
     1.5      val unfold_rex_tac = unfold_tac @{thms rex_def};
     1.6      fun prove_rex_tac ss = unfold_rex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
     1.7 -  in
     1.8 -    fn _ => fn ss => Quantifier1.rearrange_bex (prove_rex_tac ss) ss o term_of
     1.9 -  end
    1.10 +  in fn _ => fn ss => Quantifier1.rearrange_bex (prove_rex_tac ss) ss end
    1.11  *}
    1.12  
    1.13  simproc_setup defined_rall ("ALL x[M]. P(x) --> Q(x)") = {*
    1.14    let
    1.15      val unfold_rall_tac = unfold_tac @{thms rall_def};
    1.16      fun prove_rall_tac ss = unfold_rall_tac ss THEN Quantifier1.prove_one_point_all_tac;
    1.17 -  in
    1.18 -    fn _ => fn ss => Quantifier1.rearrange_ball (prove_rall_tac ss) ss o term_of
    1.19 -  end
    1.20 +  in fn _ => fn ss => Quantifier1.rearrange_ball (prove_rall_tac ss) ss end
    1.21  *}
    1.22  
    1.23  end