# HG changeset patch
# User blanchet
# Date 1360338064 -3600
# Node ID 0ee6039d2c8e3e887b709b10d3698975a5ce307a
# Parent  177db6811f11b93a044b6ef7b7b0c31c3ad5b703
distinguish one more kind of proofs

diff -r 177db6811f11 -r 0ee6039d2c8e src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Fri Feb 08 15:38:33 2013 +0100
+++ b/src/HOL/TPTP/mash_export.ML	Fri Feb 08 16:41:04 2013 +0100
@@ -83,9 +83,10 @@
       in File.append path s end
   in List.app do_fact facts end
 
+val prover_marker = "$a"
 val isar_marker = "$i"
 val omitted_marker = "$o"
-val prover_marker = "$a"
+val unprovable_marker = "$u" (* axiom or definition or characteristic theorem *)
 val prover_failed_marker = "$x"
 
 fun smart_dependencies_of ctxt params_opt facts name_tabs th isar_deps_opt =
@@ -101,7 +102,7 @@
             case isar_deps_opt of
               SOME deps => deps
             | NONE => isar_dependencies_of name_tabs th
-        in (isar_marker, deps) end
+        in (if null deps then unprovable_marker else isar_marker, deps) end
   in
     case trim_dependencies th deps of
       SOME deps => (marker, deps)