--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Mon Feb 03 15:33:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Mon Feb 03 16:53:58 2014 +0100
@@ -8,7 +8,7 @@
signature SLEDGEHAMMER_ISAR_PROOF =
sig
- type proof_method = Sledgehammer_Reconstructor.proof_method
+ type proof_method = Sledgehammer_Proof_Methods.proof_method
type label = string * int
type facts = label list * string list (* local and global facts *)
@@ -58,7 +58,7 @@
open ATP_Problem_Generate
open ATP_Proof_Reconstruct
open Sledgehammer_Util
-open Sledgehammer_Reconstructor
+open Sledgehammer_Proof_Methods
open Sledgehammer_Isar_Annotate
type label = string * int