Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Nitpick_Examples/Mono_Nits.thy
changeset 46711 f745bcc4a1e5
parent 46082 1c436a920730
child 51272 9c8d63b4b6be 
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Mon Feb 27 16:53:13 2012 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Mon Feb 27 16:56:25 2012 +0100
@@ -154,9 +154,9 @@
   end
 
 fun is_forbidden_theorem name =
-  length (space_explode "." name) <> 2 orelse
-  String.isPrefix "type_definition" (List.last (space_explode "." name)) orelse
-  String.isPrefix "arity_" (List.last (space_explode "." name)) orelse
+  length (Long_Name.explode name) <> 2 orelse
+  String.isPrefix "type_definition" (List.last (Long_Name.explode name)) orelse
+  String.isPrefix "arity_" (List.last (Long_Name.explode name)) orelse
   String.isSuffix "_def" name orelse
   String.isSuffix "_raw" name
isabelle