# HG changeset patch
# User paulson
# Date 1159803056 -7200
# Node ID 5480ec4b542dda4b06f24d1e2b239ecea30191b4
# Parent  634070b407316ea2c4dc00f038f8343fbb209ba4
restored the "length of name > 2" check for package definitions

diff -r 634070b40731 -r 5480ec4b542d src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Mon Oct 02 17:29:42 2006 +0200
+++ b/src/HOL/Tools/res_atp.ML	Mon Oct 02 17:30:56 2006 +0200
@@ -482,9 +482,11 @@
   (Sign.base_name s) mem_string ["induct","inducts","split","splits","split_asm"];
 
 (*Reject theorems with names like "List.filter.filter_list_def" or
-  "Accessible_Part.acc.defs", as these are definitions arising from packages*)
+  "Accessible_Part.acc.defs", as these are definitions arising from packages.
+  FIXME: this will also block definitions within locales*)
 fun is_package_def a =
-  String.isSuffix "_def" a orelse String.isSuffix "_defs" a;
+   length (NameSpace.unpack a) > 2 andalso 
+   String.isSuffix "_def" a  orelse  String.isSuffix "_defs" a;
 
 fun make_banned_test xs = 
   let val ht = Polyhash.mkTable (Polyhash.hash_string, op =)