--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Jun 29 09:05:37 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Jun 29 09:19:16 2010 +0200
@@ -8,7 +8,7 @@
signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
sig
type minimize_command = string list -> string
- type name_pool = Metis_Clauses.name_pool
+ type name_pool = Sledgehammer_TPTP_Format.name_pool
val metis_line: bool -> int -> int -> string list -> string
val metis_proof_text:
@@ -31,6 +31,7 @@
open Metis_Clauses
open Sledgehammer_Util
open Sledgehammer_Fact_Filter
+open Sledgehammer_TPTP_Format
type minimize_command = string list -> string