--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Mon Jan 23 17:40:31 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Mon Jan 23 17:40:32 2012 +0100
@@ -7,7 +7,7 @@
signature SLEDGEHAMMER_FILTER =
sig
- type locality = ATP_Translate.locality
+ type locality = ATP_Problem_Generate.locality
type relevance_fudge =
{local_const_multiplier : real,
@@ -62,7 +62,7 @@
structure Sledgehammer_Filter : SLEDGEHAMMER_FILTER =
struct
-open ATP_Translate
+open ATP_Problem_Generate
open Metis_Tactic
open Sledgehammer_Util