# HG changeset patch
# User blanchet
# Date 1358076500 -3600
# Node ID c0f38015a63254ebf20fd99a31defff042207d0b
# Parent  42c5fcc6f28fc046574c7ec0d08d944b76f5b836
don't generate queries with empty dependency list

diff -r 42c5fcc6f28f -r c0f38015a632 src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Sun Jan 13 12:15:44 2013 +0100
+++ b/src/HOL/TPTP/mash_export.ML	Sun Jan 13 12:28:20 2013 +0100
@@ -118,7 +118,8 @@
   generate_isar_or_prover_dependencies ctxt (SOME params)
 
 fun is_bad_query ctxt ho_atp th isar_deps =
-  Thm.legacy_get_kind th = "" orelse null isar_deps orelse
+  Thm.legacy_get_kind th = "" orelse
+  null (these (trim_dependencies th isar_deps)) orelse
   is_blacklisted_or_something ctxt ho_atp (Thm.get_name_hint th)
 
 fun generate_isar_or_prover_commands ctxt prover params_opt range thys