diff -r dd5fe091ff04 -r 47a32dd1b86e src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Mon Mar 23 19:01:15 2009 +0100
+++ b/src/HOL/Presburger.thy	Mon Mar 23 19:01:16 2009 +0100
@@ -439,12 +439,7 @@
 
 use "Tools/Qelim/presburger.ML"
 
-declaration {* fn _ =>
-  arith_tactic_add
-    (mk_arith_tactic "presburger" (fn ctxt => fn i => fn st =>
-       (warning "Trying Presburger arithmetic ...";   
-    Presburger.cooper_tac true [] [] ctxt i st)))
-*}
+setup {* Arith_Data.add_tactic "Presburger arithmetic" (K (Presburger.cooper_tac true [] [])) *}
 
 method_setup presburger = {*
 let