1.1 --- a/src/HOL/TPTP/mash_export.ML	Fri Feb 08 15:38:33 2013 +0100
     1.2 +++ b/src/HOL/TPTP/mash_export.ML	Fri Feb 08 16:41:04 2013 +0100
     1.3 @@ -83,9 +83,10 @@
     1.4        in File.append path s end
     1.5    in List.app do_fact facts end
     1.6  
     1.7 +val prover_marker = "$a"
     1.8  val isar_marker = "$i"
     1.9  val omitted_marker = "$o"
    1.10 -val prover_marker = "$a"
    1.11 +val unprovable_marker = "$u" (* axiom or definition or characteristic theorem *)
    1.12  val prover_failed_marker = "$x"
    1.13  
    1.14  fun smart_dependencies_of ctxt params_opt facts name_tabs th isar_deps_opt =
    1.15 @@ -101,7 +102,7 @@
    1.16              case isar_deps_opt of
    1.17                SOME deps => deps
    1.18              | NONE => isar_dependencies_of name_tabs th
    1.19 -        in (isar_marker, deps) end
    1.20 +        in (if null deps then unprovable_marker else isar_marker, deps) end
    1.21    in
    1.22      case trim_dependencies th deps of
    1.23        SOME deps => (marker, deps)