src/HOL/Tools/Quickcheck/exhaustive_generators.ML

 Exhaustive generators for various types.
 *)
 
 signature EXHAUSTIVE_GENERATORS =
 sig
-  val exhaustive_interpretation: string
-  val bounded_forall_interpretation: string
-  val full_exhaustive_interpretation: string
+  val exhaustive_plugin: string
+  val bounded_forall_plugin: string
+  val full_exhaustive_plugin: string
 
   val compile_generator_expr:
     Proof.context -> (term * term list) list -> bool -> int list -> (bool * term list) option * Quickcheck.report option
   val compile_generator_exprs: Proof.context -> term list -> (int -> term list option) list
   val compile_validator_exprs: Proof.context -> term list -> (int -> bool) list

 structure Exhaustive_Generators : EXHAUSTIVE_GENERATORS =
 struct
 
 (* basics *)
 
-val exhaustive_interpretation = "exhaustive"
-val bounded_forall_interpretation = "bounded_forall"
-val full_exhaustive_interpretation = "full_exhaustive"
+val exhaustive_plugin = "exhaustive"
+val bounded_forall_plugin = "bounded_forall"
+val full_exhaustive_plugin = "full_exhaustive"
 
 
 (** dynamic options **)
 
 val smart_quantifier = Attrib.setup_config_bool @{binding quickcheck_smart_quantifier} (K true)

   Quickcheck_Common.generator_test_goal_terms ("exhaustive", (size_matters_for, compile_generator_expr));
   
 (* setup *)
 
 val setup_exhaustive_datatype_interpretation =
-  Quickcheck_Common.datatype_interpretation exhaustive_interpretation
+  Quickcheck_Common.datatype_interpretation exhaustive_plugin
     (@{sort exhaustive}, instantiate_exhaustive_datatype)
 
 val setup_bounded_forall_datatype_interpretation =
-  BNF_LFP_Compat.interpretation bounded_forall_interpretation BNF_LFP_Compat.Keep_Nesting
+  BNF_LFP_Compat.interpretation bounded_forall_plugin BNF_LFP_Compat.Keep_Nesting
     (Quickcheck_Common.ensure_sort
        (((@{sort type}, @{sort type}), @{sort bounded_forall}),
        (fn thy => BNF_LFP_Compat.the_descr thy BNF_LFP_Compat.Keep_Nesting, instantiate_bounded_forall_datatype)))
 
 val active = Attrib.setup_config_bool @{binding quickcheck_exhaustive_active} (K true);
 
 val setup =
-  Quickcheck_Common.datatype_interpretation full_exhaustive_interpretation
+  Quickcheck_Common.datatype_interpretation full_exhaustive_plugin
     (@{sort full_exhaustive}, instantiate_full_exhaustive_datatype)
   #> Context.theory_map (Quickcheck.add_tester ("exhaustive", (active, test_goals)))
   #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs))
   #> Context.theory_map (Quickcheck.add_batch_validator ("exhaustive", compile_validator_exprs));