src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 48565 7c497a239007
parent 48272 db75b4005d9a
child 48568 084cd758a8ab
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Jul 27 19:27:21 2012 +0200
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Jul 27 20:05:56 2012 +0200
     1.3 @@ -249,8 +249,9 @@
     1.4            "main = getArgs >>= \\[potential, size] -> " ^
     1.5            "Narrowing_Engine.depthCheck (read potential) (read size) (Generated_Code.value ())\n\n" ^
     1.6            "}\n"
     1.7 -        val code' = prefix "module Generated_Code where {\n\ndata Typerep = Typerep String [Typerep];\n"
     1.8 -          (unprefix "module Generated_Code where {" code)
     1.9 +        val code' = code
    1.10 +          |> unsuffix "}\n"
    1.11 +          |> suffix "data Typerep = Typerep String [Typerep];\n\n}\n" (* FIXME *)
    1.12          val _ = File.write code_file code'
    1.13          val _ = File.write narrowing_engine_file
    1.14            (if contains_existentials then pnf_narrowing_engine else narrowing_engine)