src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML

   val add_new_random_dseq_equations : options -> string list -> theory -> theory
   val mk_tracing : string -> term -> term
   val prepare_intrs : options -> Proof.context -> string list -> thm list ->
     ((string * typ) list * string list * string list * (string * mode list) list *
       (string *  (Term.term list * Predicate_Compile_Aux.indprem list) list) list)
-  type mode_analysis_options = {use_random : bool, reorder_premises : bool, infer_pos_and_neg_modes : bool}  
+  type mode_analysis_options =
+   {use_generators : bool,
+    reorder_premises : bool,
+    infer_pos_and_neg_modes : bool}  
   datatype mode_derivation = Mode_App of mode_derivation * mode_derivation | Context of mode
     | Mode_Pair of mode_derivation * mode_derivation | Term of mode
   val head_mode_of : mode_derivation -> mode
   type moded_clause = term list * (Predicate_Compile_Aux.indprem * mode_derivation) list
   type 'a pred_mode_table = (string * ((bool * mode) * 'a) list) list

     | New_Neg_Random_DSeq => new_pos_random_dseq_comp_modifiers
     | c => comp_modifiers)
 
 (** mode analysis **)
 
-type mode_analysis_options = {use_random : bool, reorder_premises : bool, infer_pos_and_neg_modes : bool}
+type mode_analysis_options =
+  {use_generators : bool,
+  reorder_premises : bool,
+  infer_pos_and_neg_modes : bool}
 
 fun is_constrt thy =
   let
     val cnstrs = flat (maps
       (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)

         (case
           (select_mode_prem mode_analysis_options ctxt pred pol (modes', (pos_modes', neg_modes')) vs ps) of
           SOME (p, SOME (deriv, [])) => check_mode_prems ((p, deriv) :: acc_ps) rnd
             (known_vs_after p vs) (filter_out (equal p) ps)
         | SOME (p, SOME (deriv, missing_vars)) =>
-          if #use_random mode_analysis_options andalso pol then
+          if #use_generators mode_analysis_options andalso pol then
             check_mode_prems ((p, deriv) :: (map
               (fn v => (Generator (v, the (AList.lookup (op =) vTs v)), Term Output))
                 (distinct (op =) missing_vars))
                 @ acc_ps) true (known_vs_after p vs) (filter_out (equal p) ps)
           else NONE

       NONE => NONE
     | SOME (acc_ps, vs, rnd) =>
       if forall (is_constructable vs) (in_ts @ out_ts) then
         SOME (ts, rev acc_ps, rnd)
       else
-        if #use_random mode_analysis_options andalso pol then
+        if #use_generators mode_analysis_options andalso pol then
           let
              val generators = map
               (fn v => (Generator (v, the (AList.lookup (op =) vTs v)), Term Output))
                 (subtract (op =) vs (terms_vs (in_ts @ out_ts)))
           in

   prove : options -> theory -> (string * (term list * indprem list) list) list -> (string * typ) list
     -> moded_clause list pred_mode_table -> term pred_mode_table -> thm pred_mode_table,
   add_code_equations : Proof.context -> (string * typ) list
     -> (string * thm list) list -> (string * thm list) list,
   comp_modifiers : Comp_Mod.comp_modifiers,
-  use_random : bool,
+  use_generators : bool,
   qname : bstring
   }
 
 fun add_equations_of steps mode_analysis_options options prednames thy =
   let

     val thy'' = fold preprocess (flat scc) thy'
     val thy''' = fold_rev
       (fn preds => fn thy =>
         if not (forall (defined (ProofContext.init_global thy)) preds) then
           let
-            val mode_analysis_options = {use_random = #use_random (dest_steps steps),
+            val mode_analysis_options = {use_generators = #use_generators (dest_steps steps),
               reorder_premises =
                 not (no_topmost_reordering options andalso not (null (inter (op =) preds names))),
-              infer_pos_and_neg_modes = #use_random (dest_steps steps)}
+              infer_pos_and_neg_modes = #use_generators (dest_steps steps)}
           in
             add_equations_of steps mode_analysis_options options preds thy
           end
         else thy)
       scc thy'' |> Theory.checkpoint

       create_definitions
       options preds (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
   prove = prove,
   add_code_equations = add_code_equations,
   comp_modifiers = predicate_comp_modifiers,
-  use_random = false,
+  use_generators = false,
   qname = "equation"})
 
 val add_depth_limited_equations = gen_add_equations
   (Steps {
   define_functions =

     define_functions depth_limited_comp_modifiers PredicateCompFuns.compfuns
     options preds (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
   prove = prove_by_skip,
   add_code_equations = K (K I),
   comp_modifiers = depth_limited_comp_modifiers,
-  use_random = false,
+  use_generators = false,
   qname = "depth_limited_equation"})
 
 val add_annotated_equations = gen_add_equations
   (Steps {
   define_functions =

       define_functions annotated_comp_modifiers PredicateCompFuns.compfuns options preds
       (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
   prove = prove_by_skip,
   add_code_equations = K (K I),
   comp_modifiers = annotated_comp_modifiers,
-  use_random = false,
+  use_generators = false,
   qname = "annotated_equation"})
 
 val add_random_equations = gen_add_equations
   (Steps {
   define_functions =

       define_functions random_comp_modifiers PredicateCompFuns.compfuns options preds
       (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
   comp_modifiers = random_comp_modifiers,
   prove = prove_by_skip,
   add_code_equations = K (K I),
-  use_random = true,
+  use_generators = true,
   qname = "random_equation"})
 
 val add_depth_limited_random_equations = gen_add_equations
   (Steps {
   define_functions =

       define_functions depth_limited_random_comp_modifiers PredicateCompFuns.compfuns options preds
       (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
   comp_modifiers = depth_limited_random_comp_modifiers,
   prove = prove_by_skip,
   add_code_equations = K (K I),
-  use_random = true,
+  use_generators = true,
   qname = "depth_limited_random_equation"})
 
 val add_dseq_equations = gen_add_equations
   (Steps {
   define_functions =

     define_functions dseq_comp_modifiers DSequence_CompFuns.compfuns
     options preds (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
   prove = prove_by_skip,
   add_code_equations = K (K I),
   comp_modifiers = dseq_comp_modifiers,
-  use_random = false,
+  use_generators = false,
   qname = "dseq_equation"})
 
 val add_random_dseq_equations = gen_add_equations
   (Steps {
   define_functions =

       options preds (s, neg_modes)
     end,
   prove = prove_by_skip,
   add_code_equations = K (K I),
   comp_modifiers = pos_random_dseq_comp_modifiers,
-  use_random = true,
+  use_generators = true,
   qname = "random_dseq_equation"})
 
 val add_new_random_dseq_equations = gen_add_equations
   (Steps {
   define_functions =

       options preds (s, neg_modes)
     end,
   prove = prove_by_skip,
   add_code_equations = K (K I),
   comp_modifiers = new_pos_random_dseq_comp_modifiers,
-  use_random = true,
+  use_generators = true,
   qname = "new_random_dseq_equation"})
 
 (** user interface **)
 
 (* code_pred_intro attribute *)