# HG changeset patch
# User haftmann
# Date 1547141901 -3600
# Node ID 94048eac7463d11063b70bc2f6b90b6c7e5f8359
# Parent  e02bdf853a4c861a0f30e1d2d0d0758d983eac12
restored quickcheck/narrowing, which got accidentally broken in ef02c5e051e5

diff -r e02bdf853a4c -r 94048eac7463 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Jan 10 12:07:08 2019 +0000
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Jan 10 18:38:21 2019 +0100
@@ -236,12 +236,12 @@
         fun mk_code_file module =
           let
             val (paths, base) = split_last module
-          in Path.appends (in_path :: map Path.basic (paths @ [base ^ ".hs"])) end;
-        val generatedN = Code_Target.generatedN
-        val includes = AList.delete (op =) [generatedN] code_modules
+          in Path.appends (in_path :: map Path.basic (paths @ [suffix ".hs" base])) end;
+        val generatedN_suffix = suffix ".hs" Code_Target.generatedN;
+        val includes = AList.delete (op =) [generatedN_suffix] code_modules
           |> (map o apfst) mk_code_file
-        val code = the (AList.lookup (op =) code_modules [generatedN])
-        val code_file = mk_code_file [generatedN]
+        val code = the (AList.lookup (op =) code_modules [generatedN_suffix])
+        val code_file = mk_code_file [Code_Target.generatedN]
         val narrowing_engine_file = mk_code_file ["Narrowing_Engine"]
         val main_file = mk_code_file ["Main"]
         val main =
@@ -249,9 +249,9 @@
           "import System.IO;\n" ^
           "import System.Environment;\n" ^
           "import Narrowing_Engine;\n" ^
-          "import " ^ generatedN ^ " ;\n\n" ^
+          "import " ^ Code_Target.generatedN ^ " ;\n\n" ^
           "main = getArgs >>= \\[potential, size] -> " ^
-          "Narrowing_Engine.depthCheck (read potential) (read size) (" ^ generatedN ^
+          "Narrowing_Engine.depthCheck (read potential) (read size) (" ^ Code_Target.generatedN ^
           ".value ())\n\n}\n"
         val _ =
           map (uncurry File.write)