--- a/src/Doc/IsarRef/Spec.thy Wed Sep 11 14:07:24 2013 +0200
+++ b/src/Doc/IsarRef/Spec.thy Wed Sep 11 14:23:06 2013 +0200
@@ -251,7 +251,7 @@
Here is an artificial example of bundling various configuration
options: *}
-bundle trace = [[simp_trace, blast_trace, linarith_trace, metis_trace, smt_trace]]
+bundle trace = [[simp_trace, linarith_trace, metis_trace, smt_trace]]
lemma "x = x"
including trace by metis
--- a/src/Provers/blast.ML Wed Sep 11 14:07:24 2013 +0200
+++ b/src/Provers/blast.ML Wed Sep 11 14:23:06 2013 +0200
@@ -78,8 +78,8 @@
(* options *)
val (depth_limit, setup_depth_limit) = Attrib.config_int @{binding blast_depth_limit} (K 20);
-val (trace, setup_trace) = Attrib.config_bool @{binding blast_trace} (K false);
-val (stats, setup_stats) = Attrib.config_bool @{binding blast_stats} (K false);
+val (trace, _) = Attrib.config_bool @{binding blast_trace} (K false);
+val (stats, _) = Attrib.config_bool @{binding blast_stats} (K false);
datatype term =
@@ -1298,8 +1298,6 @@
val setup =
setup_depth_limit #>
- setup_trace #>
- setup_stats #>
Method.setup @{binding blast}
(Scan.lift (Scan.option Parse.nat) --| Method.sections Classical.cla_modifiers >>
(fn NONE => SIMPLE_METHOD' o blast_tac