src/HOL/Tools/Quickcheck/narrowing_generators.ML

 structure Narrowing_Generators : NARROWING_GENERATORS =
 struct
 
 (* configurations *)
 
-val (finite_functions, setup_finite_functions) =
-  Attrib.config_bool "quickcheck_finite_functions" (K true)
+val finite_functions = Attrib.setup_config_bool @{binding quickcheck_finite_functions} (K true)
 
 (* narrowing specific names and types *)
 
 exception FUNCTION_TYPE;
 

 
 
 val setup =
   Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
     (((@{sort typerep}, @{sort term_of}), @{sort narrowing}), instantiate_narrowing_datatype))
-  #> setup_finite_functions
   #> Context.theory_map
     (Quickcheck.add_generator ("narrowing", compile_generator_expr))
     
 end;