# HG changeset patch
# User blanchet
# Date 1410288696 -7200
# Node ID 30e7fecc9e427f4ff3fc9eea452e90d7e30c18ec
# Parent  7e353ced895eb330a0099ab097957a14e066f3f9
reverted 83a8570b44bc, which was a misunderstanding

diff -r 7e353ced895e -r 30e7fecc9e42 src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Tue Sep 09 20:51:36 2014 +0200
@@ -170,6 +170,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 (the_list isar_deps) orelse
   is_blacklisted_or_something ctxt ho_atp (Thm.get_name_hint th)