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;