merged

--- a/src/HOL/SMT.thy	Tue Jun 07 11:04:17 2011 +0200
+++ b/src/HOL/SMT.thy	Tue Jun 07 11:05:09 2011 +0200
@@ -245,14 +245,14 @@
 construction whose cycles are limited by the following option.
 *}
 
-declare [[ smt_monomorph_limit = 10 ]]
+declare [[ monomorph_max_rounds = 5 ]]
 
 text {*
 In addition, the number of generated monomorphic instances is limited
 by the following option.
 *}
 
-declare [[ smt_monomorph_instances = 500 ]]
+declare [[ monomorph_max_new_instances = 500 ]]
 
 
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Jun 07 11:04:17 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Jun 07 11:05:09 2011 +0200
@@ -544,7 +544,7 @@
 fun repair_monomorph_context max_iters max_new_instances =
   Config.put Monomorph.max_rounds max_iters
   #> Config.put Monomorph.max_new_instances max_new_instances
-  #> Config.put Monomorph.complete_instances false
+  #> Config.put Monomorph.keep_partial_instances false
 
 fun repair_smt_monomorph_context debug max_mono_iters max_mono_instances =
   (not debug ? Config.put SMT_Config.verbose false)

--- a/src/HOL/Tools/monomorph.ML	Tue Jun 07 11:04:17 2011 +0200
+++ b/src/HOL/Tools/monomorph.ML	Tue Jun 07 11:05:09 2011 +0200
@@ -37,7 +37,7 @@
   (* 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 ->
@@ -66,8 +66,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)
 
 
 
@@ -161,7 +161,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
@@ -287,7 +287,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)