# HG changeset patch
# User bulwahn
# Date 1311142595 -7200
# Node ID a1da544e2652323221bb09bf612c5f9911452529
# Parent  575bf39e078b90682424d828e172d53ffdb4dfbf
more information for the user how to deactivate quickcheck_narrowing if he does not want to use it

diff -r 575bf39e078b -r a1da544e2652 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Jul 20 08:16:33 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Jul 20 08:16:35 2011 +0200
@@ -458,7 +458,9 @@
   else
     (if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message
       ("Environment variable ISABELLE_GHC is not set. To use narrowing-based quickcheck, please set "
-        ^ "this variable to your GHC Haskell compiler in your settings file."); [Quickcheck.empty_result])
+        ^ "this variable to your GHC Haskell compiler in your settings file. "
+        ^ "To deactivate narrowing-based quickcheck, set quickcheck_narrowing_active to false.");
+      [Quickcheck.empty_result])
 
 (* setup *)