# HG changeset patch
# User noschinl
# Date 1315477391 -7200
# Node ID 8ac91e7b6024b657224fbf13ca42f0ea6e38cf77
# Parent  4bc70ab28787533d8a6fcdc150c84684b2e49ae6
call ghc with -XEmptyDataDecls

diff -r 4bc70ab28787 -r 8ac91e7b6024 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Sep 09 06:47:14 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Sep 08 12:23:11 2011 +0200
@@ -251,7 +251,7 @@
           (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"))
-        val cmd = "exec \"$ISABELLE_GHC\" -XRankNTypes -XScopedTypeVariables " ^
+        val cmd = "exec \"$ISABELLE_GHC\" -XRankNTypes -XScopedTypeVariables -XEmptyDataDecls " ^
           (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
           " -o " ^ executable ^ ";"
         val (result, compilation_time) =
diff -r 4bc70ab28787 -r 8ac91e7b6024 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Fri Sep 09 06:47:14 2011 +0200
+++ b/src/Tools/Code/code_haskell.ML	Thu Sep 08 12:23:11 2011 +0200
@@ -446,7 +446,7 @@
     (target, { serializer = serializer, literals = literals,
       check = { env_var = "ISABELLE_GHC", make_destination = I,
         make_command = fn module_name =>
-          "\"$ISABELLE_GHC\" -XRankNTypes -XScopedTypeVariables -odir build -hidir build -stubdir build -e \"\" " ^
+          "\"$ISABELLE_GHC\" -XRankNTypes -XScopedTypeVariables -XEmptyDataDecls -odir build -hidir build -stubdir build -e \"\" " ^
             module_name ^ ".hs" } })
   #> Code_Target.add_tyco_syntax target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
       brackify_infix (1, R) fxy (