src/HOL/Tools/monomorph.ML

     typ list Symtab.table
 
   (* configuration options *)
   val max_rounds: int Config.T
   val max_new_instances: int Config.T
-  val complete_instances: bool Config.T
+  val keep_partial_instances: bool Config.T
 
   (* monomorphization *)
   val monomorph: (term -> typ list Symtab.table) -> (int * thm) list ->
     Proof.context -> (int * thm) list list * Proof.context
 end

 (* configuration options *)
 
 val max_rounds = Attrib.setup_config_int @{binding monomorph_max_rounds} (K 5)
 val max_new_instances =
   Attrib.setup_config_int @{binding monomorph_max_new_instances} (K 300)
-val complete_instances =
-  Attrib.setup_config_bool @{binding monomorph_complete_instances} (K true)
+val keep_partial_instances =
+  Attrib.setup_config_bool @{binding monomorph_keep_partial_instances} (K true)
 
 
 
 (* monomorphization *)
 

 
 
 fun refine ctxt round known_grounds new_grounds (tvars, schematics) cx =
   let
     val thy = Proof_Context.theory_of ctxt
-    val count_partial = Config.get ctxt complete_instances
+    val count_partial = Config.get ctxt keep_partial_instances
 
     fun add_new_ground subst n T =
       let val T' = Envir.subst_type subst T
       in
         (* FIXME: maybe keep types in a table or net for known_grounds,

           Inttab.lookup_list subs index
           |> map_filter (with_subst tvars (instantiate theorem))
   in (map inst thm_infos, ctxt) end
 
 fun instantiate_all ctxt thm_infos (_, (_, subs, _)) =
-  if Config.get ctxt complete_instances then
+  if Config.get ctxt keep_partial_instances then
     let fun is_refined ((_, _, refined), _) = refined
     in
       (Inttab.map (K (filter_out is_refined)) subs, thm_infos)
       |-> instantiate_all' (new_super_type ctxt thm_infos)
     end