diff -r c8673078f915 -r 92715b528e78 src/HOL/Nominal/nominal_thmdecls.ML
--- a/src/HOL/Nominal/nominal_thmdecls.ML	Mon May 02 13:29:47 2011 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML	Mon May 02 16:33:21 2011 +0200
@@ -42,8 +42,7 @@
 (* equality-lemma can be derived. *)
 exception EQVT_FORM of string
 
-val (nominal_eqvt_debug, setup_nominal_eqvt_debug) =
-  Attrib.config_bool "nominal_eqvt_debug" (K false);
+val nominal_eqvt_debug = Attrib.setup_config_bool @{binding nominal_eqvt_debug} (K false);
 
 fun tactic ctxt (msg, tac) =
   if Config.get ctxt nominal_eqvt_debug
@@ -170,7 +169,6 @@
 val get_eqvt_thms = Context.Proof #> Data.get;
 
 val setup =
-  setup_nominal_eqvt_debug #>
   Attrib.setup @{binding eqvt} (Attrib.add_del eqvt_add eqvt_del) 
    "equivariance theorem declaration" #>
   Attrib.setup @{binding eqvt_force} (Attrib.add_del eqvt_force_add eqvt_force_del)