src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 44751 f523923d8182
parent 44321 975c9ba50a41
child 44852 8ac91e7b6024
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Sep 06 14:25:16 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Sep 06 16:40:22 2011 +0200
     1.3 @@ -235,17 +235,17 @@
     1.4        if Config.get ctxt overlord then with_overlord_dir else Isabelle_System.with_tmp_dir 
     1.5      fun run in_path = 
     1.6        let
     1.7 -        val code_file = Path.append in_path (Path.basic "Code.hs")
     1.8 +        val code_file = Path.append in_path (Path.basic "Generated_Code.hs")
     1.9          val narrowing_engine_file = Path.append in_path (Path.basic "Narrowing_Engine.hs")
    1.10          val main_file = Path.append in_path (Path.basic "Main.hs")
    1.11          val main = "module Main where {\n\n" ^
    1.12            "import System;\n" ^
    1.13            "import Narrowing_Engine;\n" ^
    1.14 -          "import Code;\n\n" ^
    1.15 -          "main = getArgs >>= \\[size] -> Narrowing_Engine.depthCheck (read size) (Code.value ())\n\n" ^
    1.16 +          "import Generated_Code;\n\n" ^
    1.17 +          "main = getArgs >>= \\[size] -> Narrowing_Engine.depthCheck (read size) (Generated_Code.value ())\n\n" ^
    1.18            "}\n"
    1.19 -        val code' = prefix "module Code where {\n\ndata Typerep = Typerep String [Typerep];\n"
    1.20 -          (unprefix "module Code where {" code)
    1.21 +        val code' = prefix "module Generated_Code where {\n\ndata Typerep = Typerep String [Typerep];\n"
    1.22 +          (unprefix "module Generated_Code where {" code)
    1.23          val _ = File.write code_file code'
    1.24          val _ = File.write narrowing_engine_file
    1.25            (if contains_existentials then pnf_narrowing_engine else narrowing_engine)