# HG changeset patch
# User wenzelm
# Date 1378902186 -7200
# Node ID 69c943125fd319b408f3048947cce88b4ca449f1
# Parent  24ce26e8af1296d3fc0bd585c95dbdcce5621975
do not expose internal flags to attribute name space;

diff -r 24ce26e8af12 -r 69c943125fd3 src/Doc/IsarRef/Spec.thy
--- 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
diff -r 24ce26e8af12 -r 69c943125fd3 src/Provers/blast.ML
--- 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