# HG changeset patch
# User blanchet
# Date 1322742852 -3600
# Node ID 5e547b54a9e241395094190e20cadcfaf269f234
# Parent  c7a13ce601613a1c098739469e1b165d3d67ae6c
minor example tweak

diff -r c7a13ce60161 -r 5e547b54a9e2 src/HOL/Nitpick_Examples/Mono_Nits.thy
--- 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