author | blanchet |
Mon, 08 Sep 2014 13:56:27 +0200 | |
changeset 58204 | 83a8570b44bc |
parent 58203 | 9003cc8ac94d |
child 58205 | 369513534627 |
--- a/src/HOL/TPTP/mash_export.ML Mon Sep 08 09:52:06 2014 +0200 +++ b/src/HOL/TPTP/mash_export.ML Mon Sep 08 13:56:27 2014 +0200 @@ -170,7 +170,6 @@ 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)