--- 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