--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Jun 25 16:42:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Jun 25 17:08:39 2010 +0200
@@ -8,7 +8,7 @@
signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
sig
type minimize_command = string list -> string
- type name_pool = Sledgehammer_FOL_Clause.name_pool
+ type name_pool = Metis_Clauses.name_pool
val metis_line: bool -> int -> int -> string list -> string
val metis_proof_text:
@@ -28,8 +28,8 @@
struct
open Clausifier
+open Metis_Clauses
open Sledgehammer_Util
-open Sledgehammer_FOL_Clause
type minimize_command = string list -> string