# HG changeset patch
# User wenzelm
# Date 1425897152 -3600
# Node ID 2441a80fb6c1daa6f6fad7cb630a0f6fdcf0a7e2
# Parent  ddc5411c1cb9577169967f485c44d1452660b266
eliminated unused arith "verbose" flag -- tools that need options can use the context;

diff -r ddc5411c1cb9 -r 2441a80fb6c1 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Mon Mar 09 11:21:00 2015 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML	Mon Mar 09 11:32:32 2015 +0100
@@ -907,7 +907,7 @@
     (Attrib.setup @{binding presburger}
       ((Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
         optional (keyword constsN |-- terms) >> add) "data for Cooper's algorithm"
-    #> Arith_Data.add_tactic "Presburger arithmetic" (K (tac true [] [])));
+    #> Arith_Data.add_tactic "Presburger arithmetic" (tac true [] []));
 
 end;
 
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");
 
 
diff -r ddc5411c1cb9 -r 2441a80fb6c1 src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Mon Mar 09 11:21:00 2015 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Mon Mar 09 11:32:32 2015 +0100
@@ -892,7 +892,7 @@
       METHOD (fn facts =>
         HEADGOAL (Method.insert_tac (rev (Named_Theorems.get ctxt @{named_theorems arith}) @ facts)
           THEN' tac ctxt)))) "linear arithmetic" #>
-  Arith_Data.add_tactic "linear arithmetic" (K tac);
+  Arith_Data.add_tactic "linear arithmetic" tac;
 
 val setup =
   init_arith_data
diff -r ddc5411c1cb9 -r 2441a80fb6c1 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Mon Mar 09 11:21:00 2015 +0100
+++ b/src/HOL/Word/Word.thy	Mon Mar 09 11:32:32 2015 +0100
@@ -1551,7 +1551,7 @@
 fun uint_arith_tacs ctxt = 
   let
     fun arith_tac' n t =
-      Arith_Data.verbose_arith_tac ctxt n t
+      Arith_Data.arith_tac ctxt n t
         handle Cooper.COOPER _ => Seq.empty;
   in 
     [ clarify_tac ctxt 1,
@@ -2053,7 +2053,7 @@
 fun unat_arith_tacs ctxt =   
   let
     fun arith_tac' n t =
-      Arith_Data.verbose_arith_tac ctxt n t
+      Arith_Data.arith_tac ctxt n t
         handle Cooper.COOPER _ => Seq.empty;
   in 
     [ clarify_tac ctxt 1,