# HG changeset patch
# User blanchet
# Date 1290807384 -3600
# Node ID d01a1b3ab23d592ec6f4bc44ca72ce18a4e9bd71
# Parent  a82badd0e6ef003589df797fd78a743c925fa237
renamed "trace_me{son,tis}" and "verbose_metis" to have the name of the tool first

diff -r a82badd0e6ef -r d01a1b3ab23d src/HOL/Tools/Meson/meson.ML
--- a/src/HOL/Tools/Meson/meson.ML	Fri Nov 26 22:22:07 2010 +0100
+++ b/src/HOL/Tools/Meson/meson.ML	Fri Nov 26 22:36:24 2010 +0100
@@ -46,7 +46,7 @@
 structure Meson : MESON =
 struct
 
-val (trace, trace_setup) = Attrib.config_bool "trace_meson" (K false)
+val (trace, trace_setup) = Attrib.config_bool "meson_trace" (K false)
 
 fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
 
diff -r a82badd0e6ef -r d01a1b3ab23d src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Nov 26 22:22:07 2010 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Nov 26 22:36:24 2010 +0100
@@ -31,8 +31,8 @@
 
 open Metis_Translate
 
-val (trace, trace_setup) = Attrib.config_bool "trace_metis" (K false)
-val (verbose, verbose_setup) = Attrib.config_bool "verbose_metis" (K true)
+val (trace, trace_setup) = Attrib.config_bool "metis_trace" (K false)
+val (verbose, verbose_setup) = Attrib.config_bool "metis_verbose" (K true)
 
 fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
 fun verbose_warning ctxt msg =