# HG changeset patch
# User haftmann
# Date 1343412356 -7200
# Node ID 7c497a2390070a543343df8bcbef878a31ce1acd
# Parent  12aa0cb2b4470708cd874c17a13a3e4ec1a0f89f
restored narrowing quickcheck after 6efff142bb54

diff -r 12aa0cb2b447 -r 7c497a239007 src/HOL/Quickcheck_Narrowing.thy
--- a/src/HOL/Quickcheck_Narrowing.thy	Fri Jul 27 19:27:21 2012 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy	Fri Jul 27 20:05:56 2012 +0200
@@ -165,7 +165,7 @@
   false Code_Printer.literal_numeral) ["Haskell_Quickcheck"]  *}
 
 code_type code_int
-  (Haskell_Quickcheck "Int")
+  (Haskell_Quickcheck "Prelude.Int")
 
 code_const "0 \<Colon> code_int"
   (Haskell_Quickcheck "0")
@@ -222,7 +222,7 @@
 
 consts toEnum :: "code_int => char"
 
-code_const toEnum (Haskell_Quickcheck "toEnum")
+code_const toEnum (Haskell_Quickcheck "Prelude.toEnum")
 
 consts marker :: "char"
 
diff -r 12aa0cb2b447 -r 7c497a239007 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- 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)