src/HOL/Tools/Quickcheck/narrowing_generators.ML

 Narrowing-based counterexample generation.
 *)
 
 signature NARROWING_GENERATORS =
 sig
-  val narrowing_plugin: string
   val allow_existentials : bool Config.T
   val finite_functions : bool Config.T
   val overlord : bool Config.T
   val ghc_options : string Config.T  (* FIXME prefer settings, i.e. getenv (!?) *)
   val active : bool Config.T

   val setup: theory -> theory
 end;
 
 structure Narrowing_Generators : NARROWING_GENERATORS =
 struct
-
-val narrowing_plugin = "quickcheck_narrowing"
 
 (* configurations *)
 
 val allow_existentials = Attrib.setup_config_bool @{binding quickcheck_allow_existentials} (K true)
 val finite_functions = Attrib.setup_config_bool @{binding quickcheck_finite_functions} (K true)

 val active = Attrib.setup_config_bool @{binding quickcheck_narrowing_active} (K false);
 
 val setup =
   Code.datatype_interpretation ensure_partial_term_of
   #> Code.datatype_interpretation ensure_partial_term_of_code
-  #> Quickcheck_Common.datatype_interpretation narrowing_plugin
+  #> Quickcheck_Common.datatype_interpretation @{plugin quickcheck_narrowing}
     (@{sort narrowing}, instantiate_narrowing_datatype)
   #> Context.theory_map (Quickcheck.add_tester ("narrowing", (active, test_goals)))
     
 end;