src/HOL/TPTP/mash_export.ML

--- a/src/HOL/TPTP/mash_export.ML	Mon Feb 04 09:06:20 2013 +0100
+++ b/src/HOL/TPTP/mash_export.ML	Tue Feb 05 17:19:13 2013 +0100
@@ -123,7 +123,7 @@
 fun is_bad_query ctxt ho_atp step j th isar_deps =
   j mod step <> 0 orelse
   Thm.legacy_get_kind th = "" orelse
-  null (these (trim_dependencies th isar_deps)) orelse
+  null 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, step) thys