diff -r c8673078f915 -r 92715b528e78 src/HOL/Tools/Meson/meson.ML
--- a/src/HOL/Tools/Meson/meson.ML	Mon May 02 13:29:47 2011 +0200
+++ b/src/HOL/Tools/Meson/meson.ML	Mon May 02 16:33:21 2011 +0200
@@ -40,19 +40,17 @@
   val make_meta_clause: thm -> thm
   val make_meta_clauses: thm list -> thm list
   val meson_tac: Proof.context -> thm list -> int -> tactic
-  val setup : theory -> theory
 end
 
 structure Meson : MESON =
 struct
 
-val (trace, trace_setup) = Attrib.config_bool "meson_trace" (K false)
+val trace = Attrib.setup_config_bool @{binding meson_trace} (K false)
 
 fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
 
 val max_clauses_default = 60
-val (max_clauses, max_clauses_setup) =
-  Attrib.config_int "meson_max_clauses" (K max_clauses_default)
+val max_clauses = Attrib.setup_config_int @{binding meson_max_clauses} (K max_clauses_default)
 
 (*No known example (on 1-5-2007) needs even thirty*)
 val iter_deepen_limit = 50;
@@ -738,8 +736,4 @@
     name_thms "MClause#"
       (distinct Thm.eq_thm_prop (map make_meta_clause ths));
 
-val setup =
-  trace_setup
-  #> max_clauses_setup
-
 end;