src/HOL/Tools/ATP/atp_proof.ML

   val parse_line: string -> ('a * string ATP_Problem.atp_problem_line list) list ->
     string list -> ((string * string list) * ATP_Problem.atp_formula_role *
     (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;
 
 structure ATP_Proof : ATP_PROOF =