# HG changeset patch
# User sultana
# Date 1378241200 -3600
# Node ID 74cee48bccd667f401f40a84743d17ba38323e7e
# Parent  c878390475f326fc870953d89398474dcb85b11e
brought up to date with TPTP_Proof;

diff -r c878390475f3 -r 74cee48bccd6 src/HOL/TPTP/TPTP_Parser/tptp_to_dot.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_to_dot.ML	Tue Sep 03 21:46:40 2013 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_to_dot.ML	Tue Sep 03 21:46:40 2013 +0100
@@ -78,12 +78,20 @@
        else the_role_shape role) ^
    "\", style=\"" ^ the_lang_style lang ^
    "\", label=\"" ^ n ^ "\"];\n" ^
-   (case TPTP_Proof.extract_inference_info annot of
-     NONE => ""
-   | SOME (rule, ids) =>
-       map (dot_arc reverse_arrows
-             (n, if with_label then SOME rule else NONE)) ids
-       |> implode)
+   (case TPTP_Proof.extract_source_info annot of
+        SOME (TPTP_Proof.Inference (rule, _, pinfos)) =>
+          let
+            fun parent_id (TPTP_Proof.Parent n) = n
+              | parent_id (TPTP_Proof.ParentWithDetails (n, _)) = n
+            val parent_ids = map parent_id pinfos
+          in
+            map
+              (dot_arc reverse_arrows
+               (n, if with_label then SOME rule else NONE))
+              parent_ids
+            |> implode
+          end
+      | _ => "")
  else ""
 
 (*FIXME add opts to label arcs etc*)