Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
simplified is_package_def -- be less ambitious about B library operations;
authorwenzelm
Fri, 29 Sep 2006 11:32:58 +0200
changeset 20781 e26fe5c63c2f
parent 20780 5855d1bbf210
child 20782 18abee32d1b6
simplified is_package_def -- be less ambitious about B library operations;
src/HOL/Tools/res_atp.ML file | annotate | diff | comparison | revisions 
--- 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 =)
isabelle