--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sat Aug 20 09:42:12 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sat Aug 20 09:42:34 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\" -fglasgow-exts " ^
+ val cmd = "exec \"$ISABELLE_GHC\" -XRankNTypes -XScopedTypeVariables " ^
(space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
" -o " ^ executable ^ ";"
val (result, compilation_time) =
--- a/src/Tools/Code/code_haskell.ML Sat Aug 20 09:42:12 2011 +0200
+++ b/src/Tools/Code/code_haskell.ML Sat Aug 20 09:42:34 2011 +0200
@@ -453,7 +453,7 @@
(target, { serializer = serializer, literals = literals,
check = { env_var = "ISABELLE_GHC", make_destination = I,
make_command = fn module_name =>
- "\"$ISABELLE_GHC\" -fglasgow-exts -odir build -hidir build -stubdir build -e \"\" " ^
+ "\"$ISABELLE_GHC\" -XRankNTypes -XScopedTypeVariables -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 (