# HG changeset patch # User noschinl # Date 1313667461 -7200 # Node ID 975c9ba50a41c15997dbcdaa01a3b4ec5a0f3287 # Parent 33439faadd6715bb2b06bbc93de2916c3070f562 do not call ghc with -fglasgow-exts diff -r 33439faadd67 -r 975c9ba50a41 src/HOL/Tools/Quickcheck/narrowing_generators.ML --- 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) = diff -r 33439faadd67 -r 975c9ba50a41 src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Fri Aug 19 19:01:00 2011 -0700 +++ b/src/Tools/Code/code_haskell.ML Thu Aug 18 13:37:41 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 (