--- 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))
--- 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;
--- 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