do not expose internal flags to attribute name space;
authorwenzelm
Wed, 11 Sep 2013 14:23:06 +0200
changeset 53536 69c943125fd3
parent 53533 24ce26e8af12
child 53537 addbc2387c61
do not expose internal flags to attribute name space;
src/Doc/IsarRef/Spec.thy
src/Provers/blast.ML
--- 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