proper context for cooper_tac within arith;
authorwenzelm
Tue Jul 31 19:40:25 2007 +0200 (2007-07-31)
changeset 240946db35c14146d
parent 24093 5d0ecd0c8f3c
child 24095 785c3cd7fcb5
proper context for cooper_tac within arith;
src/HOL/Presburger.thy
     1.1 --- a/src/HOL/Presburger.thy	Tue Jul 31 19:40:24 2007 +0200
     1.2 +++ b/src/HOL/Presburger.thy	Tue Jul 31 19:40:25 2007 +0200
     1.3 @@ -441,10 +441,9 @@
     1.4  
     1.5  declaration {* fn _ =>
     1.6    arith_tactic_add
     1.7 -    (mk_arith_tactic "presburger" (fn i => fn st =>
     1.8 +    (mk_arith_tactic "presburger" (fn ctxt => fn i => fn st =>
     1.9         (warning "Trying Presburger arithmetic ...";   
    1.10 -    Presburger.cooper_tac true [] [] ((ProofContext.init o theory_of_thm) st) i st)))
    1.11 -  (* FIXME!!!!!!! get the right context!!*)	
    1.12 +    Presburger.cooper_tac true [] [] ctxt i st)))
    1.13  *}
    1.14  
    1.15  method_setup presburger = {*