src/HOL/Tools/Sledgehammer/metis_tactics.ML

 open Sledgehammer_FOL_Clause
 open Sledgehammer_Fact_Preprocessor
 open Sledgehammer_HOL_Clause
 open Sledgehammer_Proof_Reconstruct
 open Sledgehammer_Fact_Filter
+open Sledgehammer_TPTP_Format
 
 val trace = Unsynchronized.ref false;
 fun trace_msg msg = if !trace then tracing (msg ()) else ();
 
 val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true);