# HG changeset patch
# User blanchet
# Date 1379021353 -7200
# Node ID 3fb81ab13ea3be5993b2b767c8571496f82267c0
# Parent  bd5fa6425993361dfe0b44b4ea020c6438e4b138
generalized data structure, for extension with SMT solver proofs

diff -r bd5fa6425993 -r 3fb81ab13ea3 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Thu Sep 12 22:10:57 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Thu Sep 12 23:29:13 2013 +0200
@@ -35,10 +35,11 @@
     UnknownError of string
 
   type atp_step_name = string * string list
-  type 'a atp_step =
-    atp_step_name * atp_formula_role * 'a * string * atp_step_name list
+  type ('a, 'b) atp_step =
+    atp_step_name * atp_formula_role * 'a * 'b * atp_step_name list
 
-  type 'a atp_proof = ('a, 'a, ('a, 'a) atp_term, 'a) atp_formula atp_step list
+  type 'a atp_proof =
+    (('a, 'a, ('a, 'a) atp_term, 'a) atp_formula, string) atp_step list
 
   val short_output : bool -> string -> string
   val string_of_atp_failure : atp_failure -> string
@@ -196,10 +197,11 @@
     | _ => raise Fail "not Vampire"
   end
 
-type 'a atp_step =
-  atp_step_name * atp_formula_role * 'a * string * atp_step_name list
+type ('a, 'b) atp_step =
+  atp_step_name * atp_formula_role * 'a * 'b * atp_step_name list
 
-type 'a atp_proof = ('a, 'a, ('a, 'a) atp_term, 'a) atp_formula atp_step list
+type 'a atp_proof =
+  (('a, 'a, ('a, 'a) atp_term, 'a) atp_formula, string) atp_step list
 
 (**** PARSING OF TSTP FORMAT ****)