# HG changeset patch
# User haftmann
# Date 1433177961 -7200
# Node ID 9251f82337d6784d51ef698c82bd56f4b58f0880
# Parent  26700f36d6f1a758cdaad07cf9ff44cfa200be4c
dropped dead config option

diff -r 26700f36d6f1 -r 9251f82337d6 src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Mon Jun 01 18:59:20 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Mon Jun 01 18:59:21 2015 +0200
@@ -135,8 +135,7 @@
     | Fastforce_Method => Clasimp.fast_force_tac ctxt
     | Force_Method => Clasimp.force_tac ctxt
     | Moura_Method => moura_tac ctxt
-    | Linarith_Method =>
-      let val ctxt = Config.put Lin_Arith.verbose false ctxt in Lin_Arith.tac ctxt end
+    | Linarith_Method => Lin_Arith.tac ctxt
     | Presburger_Method => Cooper.tac true [] [] ctxt
     | Algebra_Method => Groebner.algebra_tac [] [] ctxt))
 
diff -r 26700f36d6f1 -r 9251f82337d6 src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Mon Jun 01 18:59:20 2015 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Mon Jun 01 18:59:21 2015 +0200
@@ -21,7 +21,6 @@
   val global_setup: theory -> theory
   val split_limit: int Config.T
   val neq_limit: int Config.T
-  val verbose: bool Config.T
   val trace: bool Config.T
 end;
 
@@ -102,7 +101,6 @@
 
 val split_limit = Attrib.setup_config_int @{binding linarith_split_limit} (K 9);
 val neq_limit = Attrib.setup_config_int @{binding linarith_neq_limit} (K 9);
-val verbose = Attrib.setup_config_bool @{binding linarith_verbose} (K true);
 val trace = Attrib.setup_config_bool @{binding linarith_trace} (K false);
 
 
@@ -110,7 +108,6 @@
 struct
 
 val neq_limit = neq_limit;
-val verbose = verbose;
 val trace = trace;
 
 
diff -r 26700f36d6f1 -r 9251f82337d6 src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Mon Jun 01 18:59:20 2015 +0200
+++ b/src/HOL/Tools/try0.ML	Mon Jun 01 18:59:21 2015 +0200
@@ -105,7 +105,6 @@
    bound exceeded" warnings and the like. *)
 fun silence_methods debug =
   Config.put Metis_Tactic.verbose debug
-  #> Config.put Lin_Arith.verbose debug
   #> not debug ? (fn ctxt =>
       ctxt
       |> Context_Position.set_visible false