src/HOL/TPTP/mash_export.ML

   generate_isar_or_prover_dependencies ctxt (SOME params)
 
 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
                                      file_name =
   let