src/HOL/Nominal/nominal_thmdecls.ML

 (* the implicational case it is also checked that the variables and permutation fit  *)
 (* together, i.e. are of the right "pt_class", so that a stronger version of the     *)
 (* 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
   then tac THEN' (K (print_tac ("after " ^ msg)))
   else tac

 val eqvt_force_del  = Thm.declaration_attribute (Data.map o Thm.del_thm);
 
 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)
     "equivariance theorem declaration (without checking the form of the lemma)" #>
   Global_Theory.add_thms_dynamic (@{binding eqvts}, Data.get);