diff -r 2c6851248b3f -r 542ff50555f5 Nominal/nominal_permeq.ML
--- a/Nominal/nominal_permeq.ML	Mon May 09 04:49:58 2011 +0100
+++ b/Nominal/nominal_permeq.ML	Tue May 10 07:47:06 2011 +0100
@@ -26,7 +26,6 @@
   val args_parser: (thm list * string list) context_parser
 
   val trace_eqvt: bool Config.T
-  val setup: theory -> theory
 end;
 
 (* 
@@ -95,7 +94,7 @@
 
 
 (* tracing infrastructure *)
-val (trace_eqvt, trace_eqvt_setup) = Attrib.config_bool "trace_eqvt" (K false);
+val trace_eqvt = Attrib.setup_config_bool @{binding "trace_eqvt"} (K false);
 
 fun trace_enabled ctxt = Config.get ctxt trace_eqvt
 
@@ -211,10 +210,6 @@
 fun eqvt_tac ctxt config = 
   CONVERSION (eqvt_conv ctxt config)
 
-(* setup of the configuration value *)
-val setup =
-  trace_eqvt_setup
-
 
 (** methods **)
 fun unless_more_args scan = Scan.unless (Scan.lift ((Args.$$$ "exclude") -- Args.colon)) scan