# 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