--- 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