src/HOL/Tools/Sledgehammer/metis_tactics.ML
changeset 37566 9ca40dff25bd
parent 37548 6a7a9261b9ad
child 37572 a899f9506f39
     1.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Jun 25 12:15:49 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Jun 25 15:01:35 2010 +0200
     1.3 @@ -23,7 +23,6 @@
     1.4  open Sledgehammer_Fact_Preprocessor
     1.5  open Sledgehammer_HOL_Clause
     1.6  open Sledgehammer_Proof_Reconstruct
     1.7 -open Sledgehammer_Fact_Filter
     1.8  open Sledgehammer_TPTP_Format
     1.9  
    1.10  exception METIS of string * string