--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Jul 27 19:27:21 2012 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Jul 27 20:05:56 2012 +0200
@@ -249,8 +249,9 @@
"main = getArgs >>= \\[potential, size] -> " ^
"Narrowing_Engine.depthCheck (read potential) (read size) (Generated_Code.value ())\n\n" ^
"}\n"
- val code' = prefix "module Generated_Code where {\n\ndata Typerep = Typerep String [Typerep];\n"
- (unprefix "module Generated_Code where {" code)
+ val code' = code
+ |> unsuffix "}\n"
+ |> suffix "data Typerep = Typerep String [Typerep];\n\n}\n" (* FIXME *)
val _ = File.write code_file code'
val _ = File.write narrowing_engine_file
(if contains_existentials then pnf_narrowing_engine else narrowing_engine)