1.1 --- a/src/HOL/Tools/SMT/smt_config.ML	Wed Oct 02 22:54:42 2013 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_config.ML	Wed Oct 02 22:54:42 2013 +0200
     1.3 @@ -33,7 +33,6 @@
     1.4    val monomorph_limit: int Config.T
     1.5    val monomorph_instances: int Config.T
     1.6    val infer_triggers: bool Config.T
     1.7 -  val drop_bad_facts: bool Config.T
     1.8    val filter_only_facts: bool Config.T
     1.9    val debug_files: string Config.T
    1.10  
    1.11 @@ -161,7 +160,6 @@
    1.12  val monomorph_limit = Attrib.setup_config_int @{binding smt_monomorph_limit} (K 10)
    1.13  val monomorph_instances = Attrib.setup_config_int @{binding smt_monomorph_instances} (K 500)
    1.14  val infer_triggers = Attrib.setup_config_bool @{binding smt_infer_triggers} (K false)
    1.15 -val drop_bad_facts = Attrib.setup_config_bool @{binding smt_drop_bad_facts} (K false)
    1.16  val filter_only_facts = Attrib.setup_config_bool @{binding smt_filter_only_facts} (K false)
    1.17  val debug_files = Attrib.setup_config_string @{binding smt_debug_files} (K "")
    1.18