src/HOL/Tools/Quickcheck/narrowing_generators.ML

           "import Narrowing_Engine;\n" ^
           "import Generated_Code;\n\n" ^
           "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)
         val _ = File.write main_file main
         val executable = File.shell_path (Path.append in_path (Path.basic "isabelle_quickcheck_narrowing"))