diff -r 443708f05bb2 -r dabf6e311213 src/HOL/Tools/monomorph.ML
--- a/src/HOL/Tools/monomorph.ML	Tue Jun 07 08:58:23 2011 +0200
+++ b/src/HOL/Tools/monomorph.ML	Tue Jun 07 10:24:16 2011 +0200
@@ -38,7 +38,7 @@
   val verbose: bool Config.T
   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 ->
@@ -68,8 +68,8 @@
 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)
 
 
 
@@ -163,7 +163,7 @@
 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
@@ -289,7 +289,7 @@
   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)