src/HOL/Tools/res_atp.ML
changeset 20823 5480ec4b542d
parent 20781 e26fe5c63c2f
child 20854 f9cf9e62d11c
     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 =)