# HG changeset patch
# User blanchet
# Date 1307425494 -7200
# Node ID 142b580879748d6a513397024ec8751f38bef9a0
# Parent  97906dfd39b76caf6f8f8b91d459d7539ddf3da1
added (currently unused) verbose configuration option

diff -r 97906dfd39b7 -r 142b58087974 src/HOL/Tools/monomorph.ML
--- a/src/HOL/Tools/monomorph.ML	Tue Jun 07 07:06:24 2011 +0200
+++ b/src/HOL/Tools/monomorph.ML	Tue Jun 07 07:44:54 2011 +0200
@@ -35,6 +35,7 @@
     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
@@ -63,6 +64,7 @@
 
 (* 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)