# HG changeset patch
# User blanchet
# Date 1403782376 -7200
# Node ID 29691e2dde9a2c230aedca2684460d0c0614e1ea
# Parent  fc4d65afdf136a1d54bbd7419aede9cf70defcff
generate right dependencies in MaSh driver

diff -r fc4d65afdf13 -r 29691e2dde9a src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Mon Jun 23 12:54:48 2014 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Thu Jun 26 13:32:56 2014 +0200
@@ -90,7 +90,6 @@
 
 val prover_marker = "$a"
 val isar_marker = "$i"
-val missing_marker = "$m"
 val omitted_marker = "$o"
 val unprovable_marker = "$u" (* axiom or definition or characteristic theorem *)
 val prover_failed_marker = "$x"
@@ -109,10 +108,10 @@
               NONE => isar_dependencies_of name_tabs th
             | deps => deps)
         in
-          ((case deps of
-             NONE => missing_marker
-           | SOME [] => unprovable_marker
-           | SOME deps => isar_marker), [])
+          (case deps of
+            NONE => (omitted_marker, [])
+          | SOME [] => (unprovable_marker, [])
+          | SOME deps => (isar_marker, deps))
         end)
   in
     (case trim_dependencies deps of