diff -r 0783415ed7f0 -r ed2869dd9bfa src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Oct 22 13:54:51 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Oct 22 13:57:54 2010 +0200
@@ -23,7 +23,6 @@
 open ATP_Proof
 open Sledgehammer_Util
 open Sledgehammer_Filter
-open Sledgehammer_Translate
 open Sledgehammer
 
 (* wrapper for calling external prover *)