diff -r ddc5411c1cb9 -r 2441a80fb6c1 src/HOL/Tools/arith_data.ML
--- a/src/HOL/Tools/arith_data.ML	Mon Mar 09 11:21:00 2015 +0100
+++ b/src/HOL/Tools/arith_data.ML	Mon Mar 09 11:32:32 2015 +0100
@@ -7,8 +7,7 @@
 signature ARITH_DATA =
 sig
   val arith_tac: Proof.context -> int -> tactic
-  val verbose_arith_tac: Proof.context -> int -> tactic
-  val add_tactic: string -> (bool -> Proof.context -> int -> tactic) -> theory -> theory
+  val add_tactic: string -> (Proof.context -> int -> tactic) -> theory -> theory
 
   val mk_number: typ -> int -> term
   val mk_sum: typ -> term list -> term
@@ -29,7 +28,7 @@
 
 structure Arith_Tactics = Theory_Data
 (
-  type T = (serial * (string * (bool -> Proof.context -> int -> tactic))) list;
+  type T = (serial * (string * (Proof.context -> int -> tactic))) list;
   val empty = [];
   val extend = I;
   fun merge data : T = AList.merge (op =) (K true) data;
@@ -37,15 +36,12 @@
 
 fun add_tactic name tac = Arith_Tactics.map (cons (serial (), (name, tac)));
 
-fun gen_arith_tac verbose ctxt =
+fun arith_tac ctxt =
   let
     val tactics = Arith_Tactics.get (Proof_Context.theory_of ctxt);
-    fun invoke (_, (_, tac)) k st = tac verbose ctxt k st;
+    fun invoke (_, (_, tac)) k st = tac ctxt k st;
   in FIRST' (map invoke (rev tactics)) end;
 
-val arith_tac = gen_arith_tac false;
-val verbose_arith_tac = gen_arith_tac true;
-
 val _ =
   Theory.setup
     (Method.setup @{binding arith}
@@ -53,7 +49,7 @@
         METHOD (fn facts =>
           HEADGOAL
           (Method.insert_tac (rev (Named_Theorems.get ctxt @{named_theorems arith}) @ facts)
-            THEN' verbose_arith_tac ctxt))))
+            THEN' arith_tac ctxt))))
       "various arithmetic decision procedures");