diff -r 726590131ca1 -r 0debf65972c7 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Fri Jul 27 08:52:40 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Fri Jul 27 08:52:40 2012 +0200
@@ -52,7 +52,8 @@
     -> string * failure option
   val is_same_atp_step : step_name -> step_name -> bool
   val scan_general_id : string list -> string * string list
-  val satallax_unsat_coreN : string
+  val satallax_coreN : string
+  val z3_tptp_coreN : string
   val parse_formula :
     string list
     -> (string, 'a, (string, 'a) ho_term, string) formula * string list
@@ -154,7 +155,7 @@
 fun extract_delimited (begin_delim, end_delim) output =
   output |> first_field begin_delim |> the |> snd
          |> first_field end_delim |> the |> fst
-         |> first_field "\n" |> the |> snd
+         |> perhaps (try (first_field "\n" #> the #> snd))
   handle Option.Option => ""
 
 val tstp_important_message_delims =
@@ -461,16 +462,23 @@
    >> (fn ((((num, rule), deps), u), names) =>
           Inference_Step ((num, these names), u, rule, map (rpair []) deps))) x
 
-val satallax_unsat_coreN = "__satallax_unsat_core" (* arbitrary *)
+val satallax_coreN = "__satallax_core" (* arbitrary *)
+val z3_tptp_coreN = "__z3_tptp_core" (* arbitrary *)
+
+(* Syntax: core(<name>,[<name>,...,<name>]). *)
+fun parse_z3_tptp_line x =
+  (scan_general_id --| $$ "," --| $$ "[" -- parse_dependencies --| $$ "]"
+   >> (fn (name, names) =>
+          Inference_Step (("", name :: names), dummy_phi, z3_tptp_coreN, []))) x
 
 (* Syntax: <name> *)
 fun parse_satallax_line x =
   (scan_general_id --| Scan.option ($$ " ")
-   >> (fn s => Inference_Step ((s, [s]), dummy_phi, satallax_unsat_coreN, [])))
-      x
+   >> (fn s => Inference_Step ((s, [s]), dummy_phi, satallax_coreN, []))) x
 
 fun parse_line problem =
-  parse_tstp_line problem || parse_spass_line || parse_satallax_line
+  parse_tstp_line problem || parse_spass_line || parse_z3_tptp_line
+  || parse_satallax_line
 fun parse_proof problem tstp =
   tstp |> strip_spaces_except_between_idents
        |> raw_explode