# HG changeset patch
# User bulwahn
# Date 1300866639 -3600
# Node ID ef566ce50170f3093226e0d96076904b6bbf0dab
# Parent  904897d0c5bd6e80be084282aab7b5cef843caaf
changing Quickcheck_Narrowing's main function to enumerate the depth instead upto the depth

diff -r 904897d0c5bd -r ef566ce50170 src/HOL/Tools/Quickcheck/Narrowing_Engine.hs
--- a/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Wed Mar 23 08:50:32 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Wed Mar 23 08:50:39 2011 +0100
@@ -101,10 +101,10 @@
 
 depthCheck :: Testable a => Int -> a -> IO ();
 depthCheck d p =
-  (refute $ run (const p) 0 d) >>= (\n -> putStrLn $ "OK, required " ++ show n ++ " tests at depth " ++ show d);
+  (refute $ run (const p) 0 d) >> putStrLn ("NONE") >> hFlush stdout;
 
 smallCheck :: Testable a => Int -> a -> IO ();
-smallCheck d p = mapM_ (`depthCheck` p) [0..d] >> putStrLn ("NONE");
+smallCheck d p = mapM_ (`depthCheck` p) [0..d] >> putStrLn ("NONE") >> hFlush stdout;
 
 }
 
diff -r 904897d0c5bd -r ef566ce50170 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Mar 23 08:50:32 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Mar 23 08:50:39 2011 +0100
@@ -136,7 +136,7 @@
         val main = "module Main where {\n\n" ^
           "import Narrowing_Engine;\n" ^
           "import Code;\n\n" ^
-          "main = Narrowing_Engine.smallCheck " ^ string_of_int size ^ " (Code.value ())\n\n" ^
+          "main = Narrowing_Engine.depthCheck " ^ string_of_int size ^ " (Code.value ())\n\n" ^
           "}\n"
         val code' = prefix "module Code where {\n\ndata Typerep = Typerep String [Typerep];\n"
           (unprefix "module Code where {" code)