# HG changeset patch
# User blanchet
# Date 1314018165 -7200
# Node ID 01b8b6fcd857562af8975c9c966ab63904d414f2
# Parent  cd1e32b8d4c4754bfdb7fa196a0df503ebe0f078
removed unused configuration option

diff -r cd1e32b8d4c4 -r 01b8b6fcd857 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon Aug 22 15:02:45 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon Aug 22 15:02:45 2011 +0200
@@ -36,7 +36,6 @@
      only : bool}
 
   val trace : bool Config.T
-  val new_monomorphizer : bool Config.T
   val ignore_no_atp : bool Config.T
   val instantiate_inducts : bool Config.T
   val const_names_in_fact :
@@ -70,8 +69,6 @@
 fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
 
 (* experimental features *)
-val new_monomorphizer =
-  Attrib.setup_config_bool @{binding sledgehammer_new_monomorphizer} (K false)
 val ignore_no_atp =
   Attrib.setup_config_bool @{binding sledgehammer_ignore_no_atp} (K false)
 val instantiate_inducts =