src/HOL/Presburger.thy

--- a/src/HOL/Presburger.thy	Mon Jul 30 19:46:15 2007 +0200
+++ b/src/HOL/Presburger.thy	Tue Jul 31 00:56:26 2007 +0200
@@ -439,8 +439,8 @@
 
 use "Tools/Qelim/presburger.ML"
 
-setup {* 
-  arith_tactic_add 
+declaration {* fn _ =>
+  arith_tactic_add
     (mk_arith_tactic "presburger" (fn i => fn st =>
        (warning "Trying Presburger arithmetic ...";   
     Presburger.cooper_tac true [] [] ((ProofContext.init o theory_of_thm) st) i st)))