restored the "length of name > 2" check for package definitions
authorpaulson
Mon Oct 02 17:30:56 2006 +0200 (2006-10-02)
changeset 208235480ec4b542d
parent 20822 634070b40731
child 20824 aca7d38283bf
restored the "length of name > 2" check for package definitions
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Mon Oct 02 17:29:42 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Mon Oct 02 17:30:56 2006 +0200
     1.3 @@ -482,9 +482,11 @@
     1.4    (Sign.base_name s) mem_string ["induct","inducts","split","splits","split_asm"];
     1.5  
     1.6  (*Reject theorems with names like "List.filter.filter_list_def" or
     1.7 -  "Accessible_Part.acc.defs", as these are definitions arising from packages*)
     1.8 +  "Accessible_Part.acc.defs", as these are definitions arising from packages.
     1.9 +  FIXME: this will also block definitions within locales*)
    1.10  fun is_package_def a =
    1.11 -  String.isSuffix "_def" a orelse String.isSuffix "_defs" a;
    1.12 +   length (NameSpace.unpack a) > 2 andalso 
    1.13 +   String.isSuffix "_def" a  orelse  String.isSuffix "_defs" a;
    1.14  
    1.15  fun make_banned_test xs = 
    1.16    let val ht = Polyhash.mkTable (Polyhash.hash_string, op =)