# HG changeset patch
# User wenzelm
# Date 1185903625 -7200
# Node ID 6db35c14146db90fd075efcbe905b6991939f537
# Parent  5d0ecd0c8f3c679336f95a129c54eb41d13808a2
proper context for cooper_tac within arith;

diff -r 5d0ecd0c8f3c -r 6db35c14146d src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Tue Jul 31 19:40:24 2007 +0200
+++ b/src/HOL/Presburger.thy	Tue Jul 31 19:40:25 2007 +0200
@@ -441,10 +441,9 @@
 
 declaration {* fn _ =>
   arith_tactic_add
-    (mk_arith_tactic "presburger" (fn i => fn st =>
+    (mk_arith_tactic "presburger" (fn ctxt => fn i => fn st =>
        (warning "Trying Presburger arithmetic ...";   
-    Presburger.cooper_tac true [] [] ((ProofContext.init o theory_of_thm) st) i st)))
-  (* FIXME!!!!!!! get the right context!!*)	
+    Presburger.cooper_tac true [] [] ctxt i st)))
 *}
 
 method_setup presburger = {*