# HG changeset patch
# User blanchet
# Date 1307436369 -7200
# Node ID bd4d26327633836d2fd243047cdace30384bbf8a
# Parent  69f22ac07395cc5a038fe7bafd01112dafffe48f
removed "verbose" option -- there won't be any verbosity in there, according to Sascha (yeah)

diff -r 69f22ac07395 -r bd4d26327633 src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Tue Jun 07 10:43:18 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Tue Jun 07 10:46:09 2011 +0200
@@ -174,8 +174,7 @@
             I
           else
             map (pair 0)
-            #> rpair (ctxt |> not (Config.get ctxt verbose)
-                              ? Config.put Monomorph.verbose false)
+            #> rpair ctxt
             #-> Monomorph.monomorph Monomorph.all_schematic_consts_of
             #> fst #> maps (map (zero_var_indexes o snd)))
     val (old_skolems, props) =
diff -r 69f22ac07395 -r bd4d26327633 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Jun 07 10:43:18 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Jun 07 10:46:09 2011 +0200
@@ -539,9 +539,8 @@
    | _ => name)
   |> minimize_command
 
-fun repair_monomorph_context debug max_iters max_new_instances =
-  (not debug ? Config.put Monomorph.verbose false)
-  #> Config.put Monomorph.max_rounds max_iters
+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
 
@@ -603,7 +602,7 @@
             fun monomorphize_facts facts =
               let
                 val ctxt =
-                  ctxt |> repair_monomorph_context debug max_mono_iters
+                  ctxt |> repair_monomorph_context max_mono_iters
                                                    max_new_mono_instances
                 (* pseudo-theorem involving the same constants as the subgoal *)
                 val subgoal_th =
diff -r 69f22ac07395 -r bd4d26327633 src/HOL/Tools/monomorph.ML
--- a/src/HOL/Tools/monomorph.ML	Tue Jun 07 10:43:18 2011 +0200
+++ b/src/HOL/Tools/monomorph.ML	Tue Jun 07 10:46:09 2011 +0200
@@ -35,7 +35,6 @@
     typ list Symtab.table
 
   (* configuration options *)
-  val verbose: bool Config.T
   val max_rounds: int Config.T
   val max_new_instances: int Config.T
   val complete_instances: bool Config.T
@@ -64,7 +63,6 @@
 
 (* configuration options *)
 
-val verbose = Attrib.setup_config_bool @{binding monomorph_verbose} (K true)
 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)