--- a/src/HOL/Tools/ATP/atp_proof.ML Wed Jul 30 14:03:13 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Wed Jul 30 14:03:58 2014 +0200
@@ -99,8 +99,8 @@
(string, 'b, (string, string ATP_Problem.atp_type) ATP_Problem.atp_term,
'c) ATP_Problem.atp_formula
* string * (string * 'd list) list) list * string list
- val core_inference : 'a -> 'b -> ('b * 'b list) * ATP_Problem.atp_formula_role *
- ('c, 'd, (string, 'e) ATP_Problem.atp_term, 'f) ATP_Problem.atp_formula * 'a * 'g list
+ val core_inference : 'a -> 'b -> ('b * 'b list) * ATP_Problem.atp_formula_role *
+ ('c, 'd, (string, 'e) ATP_Problem.atp_term, 'f) ATP_Problem.atp_formula * 'a * 'g list
val vampire_step_name_ord : (string * 'a) * (string * 'a) -> order
val core_of_agsyhol_proof : string -> string list option
end;