# HG changeset patch
# User blanchet
# Date 1258478705 -3600
# Node ID 5fd36780760b955523add38da5eb8c832afd0e93
# Parent  b424b3259966a998f137fd90cfcd05a1e8e0c603# Parent  8bfe947305309d910713b30699dae35115b1c798
merged

diff -r b424b3259966 -r 5fd36780760b src/HOL/Nitpick_Examples/ROOT.ML
--- a/src/HOL/Nitpick_Examples/ROOT.ML	Tue Nov 17 15:55:30 2009 +0100
+++ b/src/HOL/Nitpick_Examples/ROOT.ML	Tue Nov 17 18:25:05 2009 +0100
@@ -5,4 +5,9 @@
 Nitpick examples.
 *)
 
-setmp_noncritical quick_and_dirty true (try use_thy) "Nitpick_Examples";
+Toplevel.debug := true;
+if getenv "KODKODI" = "" then
+  ()
+else
+  setmp_noncritical quick_and_dirty true use_thys
+                    ["Nitpick_Examples"];