--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Jun 26 11:14:40 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Jun 26 11:14:40 2012 +0200
@@ -9,7 +9,7 @@
signature ATP_PROOF_RECONSTRUCT =
sig
type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
- type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
+ type ('a, 'b, 'c, 'd) formula = ('a, 'b, 'c, 'd) ATP_Problem.formula
type 'a proof = 'a ATP_Proof.proof
type stature = ATP_Problem_Generate.stature
@@ -60,7 +60,7 @@
-> (string, string) ho_term -> term
val prop_from_atp :
Proof.context -> bool -> int Symtab.table
- -> (string, string, (string, string) ho_term) formula -> term
+ -> (string, string, (string, string) ho_term, string) formula -> term
val isar_proof_text :
Proof.context -> bool -> isar_params -> one_line_params -> string
val proof_text :
@@ -326,7 +326,8 @@
(**** INTERPRETATION OF TSTP SYNTAX TREES ****)
exception HO_TERM of (string, string) ho_term list
-exception FORMULA of (string, string, (string, string) ho_term) formula list
+exception FORMULA of
+ (string, string, (string, string) ho_term, string) formula list
exception SAME of unit
(* Type variables are given the basic sort "HOL.type". Some will later be