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