--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Aug 19 19:01:00 2011 -0700
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Aug 18 13:37:41 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) =