src/HOL/Tools/res_atp.ML
changeset 20781 e26fe5c63c2f
parent 20757 fe84fe0dfd30
child 20823 5480ec4b542d
     1.1 --- a/src/HOL/Tools/res_atp.ML	Thu Sep 28 23:43:02 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Sep 29 11:32:58 2006 +0200
     1.3 @@ -484,8 +484,7 @@
     1.4  (*Reject theorems with names like "List.filter.filter_list_def" or
     1.5    "Accessible_Part.acc.defs", as these are definitions arising from packages*)
     1.6  fun is_package_def a =
     1.7 -  let val l = NameSpace.unpack a
     1.8 -  in  length l > 2 andalso String.isSubstring "def" (List.last l)  end;
     1.9 +  String.isSuffix "_def" a orelse String.isSuffix "_defs" a;
    1.10  
    1.11  fun make_banned_test xs = 
    1.12    let val ht = Polyhash.mkTable (Polyhash.hash_string, op =)