# HG changeset patch
# User blanchet
# Date 1410177387 -7200
# Node ID 83a8570b44bc41f0f58432bed43cc49987391699
# Parent  9003cc8ac94d6361ac9bdb04d4350397247594d2
the kind is now always the empty string -- can no longer distinguish between user theorems and package theorems in a semi-reliable way

diff -r 9003cc8ac94d -r 83a8570b44bc src/HOL/TPTP/mash_export.ML
--- 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)