1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Aug 24 11:17:33 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Aug 24 11:17:33 2011 +0200
     1.3 @@ -22,6 +22,7 @@
     1.4  open ATP_Systems
     1.5  open ATP_Translate
     1.6  open Sledgehammer_Util
     1.7 +open Sledgehammer_Filter
     1.8  open Sledgehammer_Provers
     1.9  open Sledgehammer_Minimize
    1.10  open Sledgehammer_Run
    1.11 @@ -46,7 +47,6 @@
    1.12  
    1.13  (** Sledgehammer commands **)
    1.14  
    1.15 -val no_relevance_override = {add = [], del = [], only = false}
    1.16  fun add_relevance_override ns : relevance_override =
    1.17    {add = ns, del = [], only = false}
    1.18  fun del_relevance_override ns : relevance_override =