src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
changeset 36375 2482446a604c
parent 36373 66af0a49de39
child 36376 e83d52a52449
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Apr 23 16:59:48 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Apr 23 17:38:25 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Sledgehammer/sledgehammer_isar.ML
+(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_isar.ML
     Author:     Jasmin Blanchette, TU Muenchen
 
 Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax.
@@ -19,8 +19,8 @@
 
 open Sledgehammer_Util
 open ATP_Manager
-open ATP_Minimal
 open ATP_Wrapper
+open Sledgehammer_Fact_Minimizer
 
 structure K = OuterKeyword and P = OuterParse