1.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Sat Feb 22 22:06:10 2014 +0100
     1.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Sun Feb 23 10:33:43 2014 +0100
     1.3 @@ -14,8 +14,11 @@
     1.4  setup {* Code_Target.extend_target ("Haskell_Quickcheck", (Code_Haskell.target, I)) *}
     1.5  
     1.6  code_printing
     1.7 -  type_constructor typerep \<rightharpoonup> (Haskell_Quickcheck) "Typerep"
     1.8 -| constant Typerep.Typerep \<rightharpoonup> (Haskell_Quickcheck) "Typerep"
     1.9 +  code_module Typerep \<rightharpoonup> (Haskell_Quickcheck) {*
    1.10 +data Typerep = Typerep String [Typerep]
    1.11 +*}
    1.12 +| type_constructor typerep \<rightharpoonup> (Haskell_Quickcheck) "Typerep.Typerep"
    1.13 +| constant Typerep.Typerep \<rightharpoonup> (Haskell_Quickcheck) "Typerep.Typerep"
    1.14  | type_constructor integer \<rightharpoonup> (Haskell_Quickcheck) "Prelude.Int"
    1.15  
    1.16  code_reserved Haskell_Quickcheck Typerep

     2.1 --- a/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Sat Feb 22 22:06:10 2014 +0100
     2.2 +++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Sun Feb 23 10:33:43 2014 +0100
     2.3 @@ -4,6 +4,7 @@
     2.4  import Control.Exception;
     2.5  import System.IO;
     2.6  import System.Exit;
     2.7 +import qualified Typerep;
     2.8  import qualified Generated_Code;
     2.9  
    2.10  type Pos = [Int];
    2.11 @@ -67,8 +68,8 @@
    2.12  
    2.13  -- Testable
    2.14  
    2.15 -instance Show Generated_Code.Typerep where {
    2.16 -  show (Generated_Code.Typerep c ts) = "Type (\"" ++ c ++ "\", " ++ show ts ++ ")";
    2.17 +instance Show Typerep.Typerep where {
    2.18 +  show (Typerep.Typerep c ts) = "Type (\"" ++ c ++ "\", " ++ show ts ++ ")";
    2.19  };
    2.20  
    2.21  instance Show Generated_Code.Term where {

     3.1 --- a/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs	Sat Feb 22 22:06:10 2014 +0100
     3.2 +++ b/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs	Sun Feb 23 10:33:43 2014 +0100
     3.3 @@ -10,6 +10,7 @@
     3.4  import Data.Maybe
     3.5  import Data.List (partition, findIndex)
     3.6  import qualified Generated_Code
     3.7 +import qualified Typerep
     3.8  
     3.9  type Pos = [Int]
    3.10  
    3.11 @@ -156,8 +157,8 @@
    3.12  -- presentation of counterexample
    3.13  
    3.14  
    3.15 -instance Show Generated_Code.Typerep where {
    3.16 -  show (Generated_Code.Typerep c ts) = "Type (\"" ++ c ++ "\", " ++ show ts ++ ")";
    3.17 +instance Show Typerep.Typerep where {
    3.18 +  show (Typerep.Typerep c ts) = "Type (\"" ++ c ++ "\", " ++ show ts ++ ")";
    3.19  };
    3.20  
    3.21  instance Show Generated_Code.Term where {

     4.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sat Feb 22 22:06:10 2014 +0100
     4.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sun Feb 23 10:33:43 2014 +0100
     4.3 @@ -247,12 +247,9 @@
     4.4            "main = getArgs >>= \\[potential, size] -> " ^
     4.5            "Narrowing_Engine.depthCheck (read potential) (read size) (" ^ generatedN ^ ".value ())\n\n" ^
     4.6            "}\n"
     4.7 -        val code' = code
     4.8 -          |> unsuffix "}\n"
     4.9 -          |> suffix "data Typerep = Typerep String [Typerep];\n\n}\n" (* FIXME *)
    4.10          val _ = map (uncurry File.write) (includes @
    4.11            [(narrowing_engine_file, if contains_existentials then pnf_narrowing_engine else narrowing_engine),
    4.12 -           (code_file, code'), (main_file, main)])
    4.13 +           (code_file, code), (main_file, main)])
    4.14          val executable = File.shell_path (Path.append in_path (Path.basic "isabelle_quickcheck_narrowing"))
    4.15          val cmd = "exec \"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^
    4.16            ghc_options ^ " " ^