src/HOL/Sledgehammer.thy

--- a/src/HOL/Sledgehammer.thy	Thu Sep 16 09:59:32 2010 +0200
+++ b/src/HOL/Sledgehammer.thy	Thu Sep 16 11:12:08 2010 +0200
@@ -11,6 +11,7 @@
 imports Plain Hilbert_Choice
 uses
   ("Tools/ATP/atp_problem.ML")
+  ("Tools/ATP/atp_proof.ML")
   ("Tools/ATP/atp_systems.ML")
   ("~~/src/Tools/Metis/metis.ML")
   ("Tools/Sledgehammer/clausifier.ML")
@@ -92,6 +93,7 @@
 done
 
 use "Tools/ATP/atp_problem.ML"
+use "Tools/ATP/atp_proof.ML"
 use "Tools/ATP/atp_systems.ML"
 setup ATP_Systems.setup