diff -r 5855d1bbf210 -r e26fe5c63c2f src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Thu Sep 28 23:43:02 2006 +0200
+++ b/src/HOL/Tools/res_atp.ML	Fri Sep 29 11:32:58 2006 +0200
@@ -484,8 +484,7 @@
 (*Reject theorems with names like "List.filter.filter_list_def" or
   "Accessible_Part.acc.defs", as these are definitions arising from packages*)
 fun is_package_def a =
-  let val l = NameSpace.unpack a
-  in  length l > 2 andalso String.isSubstring "def" (List.last l)  end;
+  String.isSuffix "_def" a orelse String.isSuffix "_defs" a;
 
 fun make_banned_test xs = 
   let val ht = Polyhash.mkTable (Polyhash.hash_string, op =)