remove needless "open"
authorblanchet
Mon, 09 Aug 2010 12:07:59 +0200
changeset 38283 1dac99cc8dbd
parent 38282 319c59682c51
child 38284 9f98107ad8b4
remove needless "open"
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