# HG changeset patch
# User blanchet
# Date 1281348479 -7200
# Node ID 1dac99cc8dbd11b929a09e65520753c38b20103a
# Parent  319c59682c510956f21bf0d6eecfc8738cc4a10e
remove needless "open"

diff -r 319c59682c51 -r 1dac99cc8dbd src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML	Mon Aug 09 12:05:48 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML	Mon Aug 09 12:07:59 2010 +0200
@@ -18,7 +18,6 @@
 structure Sledgehammer_Fact_Minimize : SLEDGEHAMMER_FACT_MINIMIZE =
 struct
 
-open ATP_Systems
 open Sledgehammer_Util
 open Sledgehammer_Fact_Filter
 open Sledgehammer_Proof_Reconstruct