# HG changeset patch
# User blanchet
# Date 1256828788 -3600
# Node ID e61ad1690c11653de330d25162e3ec2eb59e724a
# Parent  d78f347515e0d21d5a7ba1f1771745acb0fa64c5
rename "NitpickMono" to "Nitpick_Mono" in example

diff -r d78f347515e0 -r e61ad1690c11 src/HOL/Nitpick_Examples/Mono_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Thu Oct 29 15:26:00 2009 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Thu Oct 29 16:06:28 2009 +0100
@@ -28,7 +28,7 @@
    skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
    unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref []}
 (* term -> bool *)
-val is_mono = NitpickMono.formulas_monotonic ext_ctxt @{typ 'a} [] []
+val is_mono = Nitpick_Mono.formulas_monotonic ext_ctxt @{typ 'a} [] []
 fun is_const t =
   let val T = fastype_of t in
     is_mono (Logic.mk_implies (Logic.mk_equals (Free ("dummyP", T), t),