1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Aug 19 19:01:00 2011 -0700
1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Aug 18 13:37:41 2011 +0200
1.3 @@ -251,7 +251,7 @@
1.4 (if contains_existentials then pnf_narrowing_engine else narrowing_engine)
1.5 val _ = File.write main_file main
1.6 val executable = File.shell_path (Path.append in_path (Path.basic "isabelle_quickcheck_narrowing"))
1.7 - val cmd = "exec \"$ISABELLE_GHC\" -fglasgow-exts " ^
1.8 + val cmd = "exec \"$ISABELLE_GHC\" -XRankNTypes -XScopedTypeVariables " ^
1.9 (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
1.10 " -o " ^ executable ^ ";"
1.11 val (result, compilation_time) =
2.1 --- a/src/Tools/Code/code_haskell.ML Fri Aug 19 19:01:00 2011 -0700
2.2 +++ b/src/Tools/Code/code_haskell.ML Thu Aug 18 13:37:41 2011 +0200
2.3 @@ -453,7 +453,7 @@
2.4 (target, { serializer = serializer, literals = literals,
2.5 check = { env_var = "ISABELLE_GHC", make_destination = I,
2.6 make_command = fn module_name =>
2.7 - "\"$ISABELLE_GHC\" -fglasgow-exts -odir build -hidir build -stubdir build -e \"\" " ^
2.8 + "\"$ISABELLE_GHC\" -XRankNTypes -XScopedTypeVariables -odir build -hidir build -stubdir build -e \"\" " ^
2.9 module_name ^ ".hs" } })
2.10 #> Code_Target.add_tyco_syntax target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
2.11 brackify_infix (1, R) fxy (