diff -r aa43c6f05bca -r 3ad2759acc52 src/HOL/Tools/arith_data.ML
--- a/src/HOL/Tools/arith_data.ML	Wed Oct 29 14:14:36 2014 +0100
+++ b/src/HOL/Tools/arith_data.ML	Wed Oct 29 14:40:14 2014 +0100
@@ -20,8 +20,6 @@
   val prove_conv2: tactic -> (Proof.context -> tactic) -> Proof.context -> term * term -> thm
   val simp_all_tac: thm list -> Proof.context -> tactic
   val simplify_meta_eq: thm list -> Proof.context -> thm -> thm
-
-  val setup: theory -> theory
 end;
 
 structure Arith_Data: ARITH_DATA =
@@ -48,14 +46,15 @@
 val arith_tac = gen_arith_tac false;
 val verbose_arith_tac = gen_arith_tac true;
 
-val setup =
-  Method.setup @{binding arith}
-    (Scan.succeed (fn ctxt =>
-      METHOD (fn facts =>
-        HEADGOAL
-        (Method.insert_tac (rev (Named_Theorems.get ctxt @{named_theorems arith}) @ facts)
-          THEN' verbose_arith_tac ctxt))))
-    "various arithmetic decision procedures";
+val _ =
+  Theory.setup
+    (Method.setup @{binding arith}
+      (Scan.succeed (fn ctxt =>
+        METHOD (fn facts =>
+          HEADGOAL
+          (Method.insert_tac (rev (Named_Theorems.get ctxt @{named_theorems arith}) @ facts)
+            THEN' verbose_arith_tac ctxt))))
+      "various arithmetic decision procedures");
 
 
 (* some specialized syntactic operations *)