# 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