make configuration of (SMT) full monomorphization more flexible: turn boolean argument into a configuration option

--- a/src/HOL/Tools/SMT/smt_config.ML	Fri Apr 01 10:18:20 2011 +0200
+++ b/src/HOL/Tools/SMT/smt_config.ML	Fri Apr 01 11:54:51 2011 +0200
@@ -33,6 +33,7 @@
   val trace_used_facts: bool Config.T
   val monomorph_limit: int Config.T
   val monomorph_instances: int Config.T
+  val monomorph_full: bool Config.T
   val infer_triggers: bool Config.T
   val drop_bad_facts: bool Config.T
   val filter_only_facts: bool Config.T
@@ -181,6 +182,10 @@
 val (monomorph_instances, setup_monomorph_instances) =
   Attrib.config_int monomorph_instancesN (K 500)
 
+val monomorph_fullN = "smt_monomorph_full"
+val (monomorph_full, setup_monomorph_full) =
+  Attrib.config_bool monomorph_fullN (K true)
+
 val infer_triggersN = "smt_infer_triggers"
 val (infer_triggers, setup_infer_triggers) =
   Attrib.config_bool infer_triggersN (K false)
@@ -207,6 +212,7 @@
   setup_verbose #>
   setup_monomorph_limit #>
   setup_monomorph_instances #>
+  setup_monomorph_full #>
   setup_infer_triggers #>
   setup_drop_bad_facts #>
   setup_filter_only_facts #>

--- a/src/HOL/Tools/SMT/smt_monomorph.ML	Fri Apr 01 10:18:20 2011 +0200
+++ b/src/HOL/Tools/SMT/smt_monomorph.ML	Fri Apr 01 11:54:51 2011 +0200
@@ -29,7 +29,7 @@
 signature SMT_MONOMORPH =
 sig
   val typ_has_tvars: typ -> bool
-  val monomorph: bool -> ('a * thm) list -> Proof.context ->
+  val monomorph: ('a * thm) list -> Proof.context ->
     ('a * thm) list * Proof.context
 end
 
@@ -197,7 +197,7 @@
 
 (* overall procedure *)
 
-fun mono_all full ctxt polys monos =
+fun mono_all ctxt polys monos =
   let
     val scss = map (single o pair Vartab.empty o tvar_consts_of o snd) polys
 
@@ -211,6 +211,7 @@
 
     val limit = Config.get ctxt SMT_Config.monomorph_limit
     val instances = Config.get ctxt SMT_Config.monomorph_instances
+    val full = Config.get ctxt SMT_Config.monomorph_full
   in
     scss
     |> search_substitutions ctxt limit instances Symtab.empty grounds
@@ -219,10 +220,10 @@
     |-> fold2 (instantiate full) polys
   end
 
-fun monomorph full irules ctxt =
+fun monomorph irules ctxt =
   irules
   |> List.partition (Term.exists_type typ_has_tvars o Thm.prop_of o snd)
   |>> incr_indexes  (* avoid clashes of schematic type variables *)
-  |-> (fn [] => rpair ctxt | polys => mono_all full ctxt polys)
+  |-> (fn [] => rpair ctxt | polys => mono_all ctxt polys)
 
 end

--- a/src/HOL/Tools/SMT/smt_normalize.ML	Fri Apr 01 10:18:20 2011 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Fri Apr 01 11:54:51 2011 +0200
@@ -631,7 +631,7 @@
   |> gen_normalize ctxt
   |> unfold1 ctxt
   |> rpair ctxt
-  |-> SMT_Monomorph.monomorph true
+  |-> SMT_Monomorph.monomorph
   |-> unfold2
   |-> apply_extra_norms
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Apr 01 10:18:20 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Apr 01 11:54:51 2011 +0200
@@ -355,7 +355,7 @@
         val (mono_facts, ctxt') =
           ctxt |> Config.put SMT_Config.verbose debug
                |> Config.put SMT_Config.monomorph_limit monomorphize_limit
-               |> SMT_Monomorph.monomorph true indexed_facts
+               |> SMT_Monomorph.monomorph indexed_facts
       in
         mono_facts
         |> sort (int_ord o pairself fst)