1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Aug 24 11:17:33 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Aug 24 11:17:33 2011 +0200
     1.3 @@ -38,6 +38,7 @@
     1.4    val trace : bool Config.T
     1.5    val ignore_no_atp : bool Config.T
     1.6    val instantiate_inducts : bool Config.T
     1.7 +  val no_relevance_override : relevance_override
     1.8    val const_names_in_fact :
     1.9      theory -> (string * typ -> term list -> bool * term list) -> term
    1.10      -> string list
    1.11 @@ -100,6 +101,8 @@
    1.12     del : (Facts.ref * Attrib.src list) list,
    1.13     only : bool}
    1.14  
    1.15 +val no_relevance_override = {add = [], del = [], only = false}
    1.16 +
    1.17  val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
    1.18  val abs_name = sledgehammer_prefix ^ "abs"
    1.19  val skolem_prefix = sledgehammer_prefix ^ "sko"