--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Thu Dec 01 12:25:27 2011 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Thu Dec 01 13:34:12 2011 +0100
@@ -8,7 +8,7 @@
header {* Examples Featuring Nitpick's Monotonicity Check *}
theory Mono_Nits
-imports Main (* "~/afp/thys/AVL-Trees/AVL2" "~/afp/thys/Huffman/Huffman" *)
+imports Main (* "~/afp/thys/DPT-SAT-Solver/DPT_SAT_Solver" "~/afp/thys/AVL-Trees/AVL2" "~/afp/thys/Huffman/Huffman" *)
begin
ML {*
@@ -153,6 +153,7 @@
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
String.isSuffix "_def" name orelse
String.isSuffix "_raw" name